{-|
Module      : Idris.Elab.Data
Description : Code to elaborate data structures.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE CPP, PatternGuards #-}
module Idris.Elab.Data(elabData) where

import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Delaborate
import Idris.Docstrings
import Idris.Elab.Rewrite
import Idris.Elab.Type
import Idris.Elab.Utils
import Idris.Elab.Value
import Idris.Error
import Idris.Output (iWarn, sendHighlighting)

import Util.Pretty

#if (MIN_VERSION_base(4,11,0))
import Prelude hiding (id, (.), (<>))
#else
import Prelude hiding (id, (.))
#endif

import Control.Category
import Control.Monad
import Data.List
import qualified Data.Set as S

warnLC :: FC -> Name -> Idris ()
warnLC :: FC -> Name -> Idris ()
warnLC FC
fc Name
n
   = FC -> OutputDoc -> Idris ()
iWarn FC
fc (OutputDoc -> Idris ()) -> OutputDoc -> Idris ()
forall a b. (a -> b) -> a -> b
$ Name -> OutputDoc
annName Name
n OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> String -> OutputDoc
forall a. String -> Doc a
text String
"has a name which may be implicitly bound."
           OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<> OutputDoc
forall a. Doc a
line OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<> String -> OutputDoc
forall a. String -> Doc a
text String
"This is likely to lead to problems!"

elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()
elabData :: ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> DataOpts
-> PData
-> Idris ()
elabData ElabInfo
info SyntaxInfo
syn Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs FC
fc DataOpts
opts (PLaterdecl Name
n FC
nfc PTerm
t_in)
    = do Int -> String -> Idris ()
logElab Int
1 ((FC, Docstring (Either Err PTerm)) -> String
forall a. Show a => a -> String
show (FC
fc, Docstring (Either Err PTerm)
doc))
         FC -> Name -> Idris ()
checkUndefined FC
fc Name
n
         Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name -> Bool
implicitable (Name -> Name
nsroot Name
n)) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> Name -> Idris ()
warnLC FC
fc Name
n
         (Type
cty, Type
_, PTerm
t, [(Int, Name)]
inacc) <- ElabInfo
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> PTerm
-> Idris (Type, Type, PTerm, [(Int, Name)])
buildType ElabInfo
info SyntaxInfo
syn FC
fc [] Name
n PTerm
t_in

         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
n)
         (Context -> Context) -> Idris ()
updateContext (Name -> NameType -> Type -> Context -> Context
addTyDecl Name
n (Int -> Int -> NameType
TCon Int
0 Int
0) Type
cty) -- temporary, to check cons
         Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting (Set (FC', OutputAnnotation) -> Idris ())
-> Set (FC', OutputAnnotation) -> Idris ()
forall a b. (a -> b) -> a -> b
$ [(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation)
forall a. Ord a => [a] -> Set a
S.fromList [(FC -> FC'
FC' FC
nfc, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing)]

elabData ElabInfo
info SyntaxInfo
syn Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs FC
fc DataOpts
opts (PDatadecl Name
n FC
nfc PTerm
t_in [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
  [Name])]
dcons)
    = do let codata :: Bool
codata = DataOpt
Codata DataOpt -> DataOpts -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` DataOpts
opts
         Int -> String -> Idris ()
logElab Int
1 (FC -> String
forall a. Show a => a -> String
show FC
fc)
         Bool
undef <- FC -> Name -> Idris Bool
isUndefined FC
fc Name
n
         Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name -> Bool
implicitable (Name -> Name
nsroot Name
n)) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> Name -> Idris ()
warnLC FC
fc Name
n
         (Type
cty, Type
ckind, PTerm
t, [(Int, Name)]
inacc) <- ElabInfo
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> PTerm
-> Idris (Type, Type, PTerm, [(Int, Name)])
buildType ElabInfo
info SyntaxInfo
syn FC
fc [] Name
n PTerm
t_in
         -- if n is defined already, make sure it is just a type declaration
         -- with the same type we've just elaborated, and no constructors
         -- yet
         IState
i <- Idris IState
getIState
         FC -> Name -> Type -> IState -> Idris ()
checkDefinedAs FC
fc Name
n Type
cty IState
i
         -- temporary, to check cons
         Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
undef (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ (Context -> Context) -> Idris ()
updateContext (Name -> NameType -> Type -> Context -> Context
addTyDecl Name
n (Int -> Int -> NameType
TCon Int
0 Int
0) Type
cty)
         let cnameinfo :: ElabInfo
cnameinfo = ElabInfo -> [Name] -> ElabInfo
cinfo ElabInfo
info (((Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
  [Name])
 -> Name)
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
     [Name])]
-> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Docstring (Either Err PTerm),
 [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
 [Name])
-> Name
forall {a} {b} {c} {d} {e} {f} {g}. (a, b, c, d, e, f, g) -> c
cname [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
  [Name])]
dcons)
         Bool
unique <- case Type -> Type
forall n. TT n -> TT n
getRetTy (Context -> Env -> Type -> Type
normalise (IState -> Context
tt_ctxt IState
i) [] Type
cty) of
                        UType Universe
UniqueType -> Bool -> Idris Bool
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                        UType Universe
_ -> Bool -> Idris Bool
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                        TType UExp
_ -> Bool -> Idris Bool
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                        Type
rt -> TC Bool -> Idris Bool
forall a. TC a -> Idris a
tclift (TC Bool -> Idris Bool) -> TC Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ Err -> TC Bool
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Name -> Maybe Type -> Err -> Err
forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating String
"type constructor " Name
n Maybe Type
forall a. Maybe a
Nothing (String -> Err
forall t. String -> Err' t
Msg String
"Not a valid type constructor")))
         [(Name, Type)]
cons <- ((Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
  [Name])
 -> StateT IState (ExceptT Err IO) (Name, Type))
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
     [Name])]
-> StateT IState (ExceptT Err IO) [(Name, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ElabInfo
-> SyntaxInfo
-> Name
-> Bool
-> Type
-> Type
-> (Docstring (Either Err PTerm),
    [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
    [Name])
-> StateT IState (ExceptT Err IO) (Name, Type)
elabCon ElabInfo
cnameinfo SyntaxInfo
syn Name
n Bool
codata (Type -> Type
forall n. TT n -> TT n
getRetTy Type
cty) Type
ckind) [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
  [Name])]
dcons
         Int
ttag <- Idris Int
getName

         Context
ctxt <- Idris Context
getContext
         let params :: [Int]
params = Name -> Type -> [Type] -> [Int]
findParams Name
n (Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
cty) (((Name, Type) -> Type) -> [(Name, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Type
forall a b. (a, b) -> b
snd [(Name, Type)]
cons)

         Int -> String -> Idris ()
logElab Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Parameters : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
forall a. Show a => a -> String
show [Int]
params
         FC -> [Int] -> Type -> [(Name, Type)] -> Idris ()
addParamConstraints FC
fc [Int]
params Type
cty [(Name, Type)]
cons

         IState
i <- Idris IState
getIState
         -- TI contains information about mutually declared types - this will
         -- be updated when the mutual block is complete
         IState -> Idris ()
putIState (IState
i { idris_datatypes =
                          addDef n (TI (map fst cons) codata opts params [n]
                                             (any linearArg (map snd cons)))
                                             (idris_datatypes i) })
         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
n)
         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCData Name
n)
         FC -> [(Name, Docstring (Either Err PTerm))] -> PTerm -> Idris ()
forall a. FC -> [(Name, Docstring a)] -> PTerm -> Idris ()
checkDocs FC
fc [(Name, Docstring (Either Err PTerm))]
argDocs PTerm
t
         Docstring DocTerm
doc' <- ElabInfo
-> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms ElabInfo
info Docstring (Either Err PTerm)
doc
         [(Name, Docstring DocTerm)]
argDocs' <- ((Name, Docstring (Either Err PTerm))
 -> StateT IState (ExceptT Err IO) (Name, Docstring DocTerm))
-> [(Name, Docstring (Either Err PTerm))]
-> StateT IState (ExceptT Err IO) [(Name, Docstring DocTerm)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(Name
n, Docstring (Either Err PTerm)
d) -> do Docstring DocTerm
d' <- ElabInfo
-> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms ElabInfo
info Docstring (Either Err PTerm)
d
                                         (Name, Docstring DocTerm)
-> StateT IState (ExceptT Err IO) (Name, Docstring DocTerm)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, Docstring DocTerm
d')) [(Name, Docstring (Either Err PTerm))]
argDocs
         Name
-> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
addDocStr Name
n Docstring DocTerm
doc' [(Name, Docstring DocTerm)]
argDocs'
         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDoc Name
n)
         let metainf :: MetaInformation
metainf = [Int] -> MetaInformation
DataMI [Int]
params
         IBCWrite -> Idris ()
addIBC (Name -> MetaInformation -> IBCWrite
IBCMetaInformation Name
n MetaInformation
metainf)
         -- TMP HACK! Make this a data option
         (Context -> Context) -> Idris ()
updateContext (Datatype Name -> Context -> Context
addDatatype (Name -> Int -> Type -> Bool -> [(Name, Type)] -> Datatype Name
forall n. n -> Int -> TT n -> Bool -> [(n, TT n)] -> Datatype n
Data Name
n Int
ttag Type
cty Bool
unique [(Name, Type)]
cons))
         (Context -> Context) -> Idris ()
updateContext (Name -> MetaInformation -> Context -> Context
setMetaInformation Name
n MetaInformation
metainf)

         ((FC, Name) -> Idris ()) -> [(FC, Name)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris ()
totcheck ([FC] -> [Name] -> [(FC, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip (FC -> [FC]
forall a. a -> [a]
repeat FC
fc) (((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
cons))
--          mapM_ (checkPositive n) cons

         -- if there's exactly one constructor,
         -- mark both the type and the constructor as detaggable
         case [(Name, Type)]
cons of
            [(Name
cn,Type
ct)] -> Name -> Idris ()
setDetaggable Name
cn Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Name -> Idris ()
setDetaggable Name
n
                Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCOpt Name
cn) Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCOpt Name
n)
            [(Name, Type)]
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

         -- create a rewriting lemma
         Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= String -> Name
sUN String
"=") (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
            ElabInfo -> Name -> Type -> Idris ()
elabRewriteLemma ElabInfo
info Name
n Type
cty
         -- Emit highlighting info
         Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting (Set (FC', OutputAnnotation) -> Idris ())
-> Set (FC', OutputAnnotation) -> Idris ()
forall a b. (a -> b) -> a -> b
$ [(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation)
forall a. Ord a => [a] -> Set a
S.fromList ([(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation))
-> [(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ [(FC -> FC'
FC' FC
nfc, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing)] [(FC', OutputAnnotation)]
-> [(FC', OutputAnnotation)] -> [(FC', OutputAnnotation)]
forall a. [a] -> [a] -> [a]
++
           ((Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
  [Name])
 -> (FC', OutputAnnotation))
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
     [Name])]
-> [(FC', OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Docstring (Either Err PTerm)
_, [(Name, Docstring (Either Err PTerm))]
_, Name
n, FC
nfc, PTerm
_, FC
_, [Name]
_) ->
                 (FC -> FC'
FC' FC
nfc, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing))
               [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
  [Name])]
dcons
  where
        checkDefinedAs :: FC -> Name -> Type -> IState -> Idris ()
checkDefinedAs FC
fc Name
n Type
t IState
i
            = let defined :: Idris a
defined = TC a -> Idris a
forall a. TC a -> Idris a
tclift (TC a -> Idris a) -> TC a -> Idris a
forall a b. (a -> b) -> a -> b
$ Err -> TC a
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Name -> Err
forall t. Name -> Err' t
AlreadyDefined Name
n))
                  ctxt :: Context
ctxt = IState -> Context
tt_ctxt IState
i in
                case Name -> Context -> [Def]
lookupDef Name
n Context
ctxt of
                   [] -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                   [TyDecl NameType
_ Type
ty] ->
                      case Context -> Env -> Type -> Type -> TC ()
converts Context
ctxt [] Type
t Type
ty of
                           OK () -> case Name -> Ctxt TypeInfo -> Maybe TypeInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
i) of
                                         Maybe TypeInfo
Nothing -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                         Maybe TypeInfo
_ -> Idris ()
forall {a}. Idris a
defined
                           TC ()
_ -> Idris ()
forall {a}. Idris a
defined
                   [Def]
_ -> Idris ()
forall {a}. Idris a
defined


        cname :: (a, b, c, d, e, f, g) -> c
cname (a
_, b
_, c
n, d
_, e
_, f
_, g
_) = c
n

        -- Abuse of ElabInfo.
        -- TODO Contemplate whether the ElabInfo type needs modification.
        cinfo :: ElabInfo -> [Name] -> ElabInfo
        cinfo :: ElabInfo -> [Name] -> ElabInfo
cinfo ElabInfo
info [Name]
ds
          = let newps :: [(Name, PTerm)]
newps = ElabInfo -> [(Name, PTerm)]
params ElabInfo
info
                dsParams :: [(Name, [a])]
dsParams = (Name -> (Name, [a])) -> [Name] -> [(Name, [a])]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, [])) [Name]
ds
                newb :: Ctxt [Name]
newb = [(Name, [Name])] -> Ctxt [Name] -> Ctxt [Name]
forall a. [(Name, a)] -> Ctxt a -> Ctxt a
addAlist [(Name, [Name])]
forall {a}. [(Name, [a])]
dsParams (ElabInfo -> Ctxt [Name]
inblock ElabInfo
info) in
                ElabInfo
info { params = newps,
                       inblock = newb,
                       liftname = id -- Is this appropriate?
                     }

elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
           Type -> -- for unique kind checking
           Type -> -- data type's kind
           (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name]) ->
           Idris (Name, Type)
elabCon :: ElabInfo
-> SyntaxInfo
-> Name
-> Bool
-> Type
-> Type
-> (Docstring (Either Err PTerm),
    [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
    [Name])
-> StateT IState (ExceptT Err IO) (Name, Type)
elabCon ElabInfo
info SyntaxInfo
syn Name
tn Bool
codata Type
expkind Type
dkind (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
argDocs, Name
n, FC
nfc, PTerm
t_in, FC
fc, [Name]
forcenames)
    = do FC -> Name -> Idris ()
checkUndefined FC
fc Name
n
         Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name -> Bool
implicitable (Name -> Name
nsroot Name
n)) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> Name -> Idris ()
warnLC FC
fc Name
n
         Int -> String -> Idris ()
logElab Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> String
forall a. Show a => a -> String
show FC
fc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":Constructor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
forall a. Show a => a -> String
show PTerm
t_in
         (Type
cty, Type
ckind, PTerm
t, [(Int, Name)]
inacc) <- ElabInfo
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> PTerm
-> Idris (Type, Type, PTerm, [(Int, Name)])
buildType ElabInfo
info SyntaxInfo
syn FC
fc [FnOpt
Constructor] Name
n (if Bool
codata then PTerm -> PTerm
mkLazy PTerm
t_in else PTerm
t_in)
         Context
ctxt <- Idris Context
getContext
         let cty' :: Type
cty' = Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
cty
         Type -> Type -> Idris ()
forall {n} {n}. TT n -> TT n -> Idris ()
checkUniqueKind Type
ckind Type
expkind

         -- Check that the constructor type is, in fact, a part of the family being defined
         Name -> Type -> Idris ()
tyIs Name
n Type
cty'
         -- Need to calculate forceability from the non-normalised type,
         -- because we might not be able to export the definitions which
         -- we're normalising which changes the forceability status!
         let force :: [Int]
force = if Name
tn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"Delayed"
                        then [] -- TMP HACK! Totality checker needs this info
                        else Context -> Name -> Type -> [Int]
forceArgs Context
ctxt Name
tn Type
cty

         Int -> String -> Idris ()
logElab Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> String
forall a. Show a => a -> String
show FC
fc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":Constructor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" elaborated : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
forall a. Show a => a -> String
show PTerm
t
         Int -> String -> Idris ()
logElab Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Inaccessible args: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Int, Name)] -> String
forall a. Show a => a -> String
show [(Int, Name)]
inacc
         Int -> String -> Idris ()
logElab Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Forceable args: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
forall a. Show a => a -> String
show [Int]
force
         Int -> String -> Idris ()
logElab Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"---> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
cty

         -- Add to the context (this is temporary, so that later constructors
         -- can be indexed by it)
         (Context -> Context) -> Idris ()
updateContext (Name -> NameType -> Type -> Context -> Context
addTyDecl Name
n (Int -> Int -> Bool -> NameType
DCon Int
0 Int
0 Bool
False) Type
cty)

         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
n)
         FC -> [(Name, Docstring (Either Err PTerm))] -> PTerm -> Idris ()
forall a. FC -> [(Name, Docstring a)] -> PTerm -> Idris ()
checkDocs FC
fc [(Name, Docstring (Either Err PTerm))]
argDocs PTerm
t
         Docstring DocTerm
doc' <- ElabInfo
-> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms ElabInfo
info Docstring (Either Err PTerm)
doc
         [(Name, Docstring DocTerm)]
argDocs' <- ((Name, Docstring (Either Err PTerm))
 -> StateT IState (ExceptT Err IO) (Name, Docstring DocTerm))
-> [(Name, Docstring (Either Err PTerm))]
-> StateT IState (ExceptT Err IO) [(Name, Docstring DocTerm)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(Name
n, Docstring (Either Err PTerm)
d) -> do Docstring DocTerm
d' <- ElabInfo
-> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms ElabInfo
info Docstring (Either Err PTerm)
d
                                         (Name, Docstring DocTerm)
-> StateT IState (ExceptT Err IO) (Name, Docstring DocTerm)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, Docstring DocTerm
d')) [(Name, Docstring (Either Err PTerm))]
argDocs
         Name
-> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
addDocStr Name
n Docstring DocTerm
doc' [(Name, Docstring DocTerm)]
argDocs'
         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDoc Name
n)
         Field IState [(Int, Name)] -> [(Int, Name)] -> Idris ()
forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState (Field OptInfo [(Int, Name)]
opt_inaccessible Field OptInfo [(Int, Name)]
-> Field IState OptInfo -> Field IState [(Int, Name)]
forall b c a. Field b c -> Field a b -> Field a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState OptInfo
ist_optimisation Name
n) [(Int, Name)]
inacc
         Field IState [Int] -> [Int] -> Idris ()
forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState (Field OptInfo [Int]
opt_forceable Field OptInfo [Int] -> Field IState OptInfo -> Field IState [Int]
forall b c a. Field b c -> Field a b -> Field a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState OptInfo
ist_optimisation Name
n) [Int]
force
         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCOpt Name
n)
         (Name, Type) -> StateT IState (ExceptT Err IO) (Name, Type)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, Type
cty)
  where
    tyIs :: Name -> Type -> Idris ()
tyIs Name
con (Bind Name
n Binder Type
b Type
sc) = Name -> Type -> Idris ()
tyIs Name
con (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
forall n. TT n
Erased) Type
sc)
    tyIs Name
con Type
t | (P NameType
Bound Name
n' Type
_, [Type]
_) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
t
        = if Name
n' Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
tn then
               TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Name -> Maybe Type -> Err -> Err
forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating String
"constructor " Name
con Maybe Type
forall a. Maybe a
Nothing
                         (String -> Err
forall t. String -> Err' t
Msg (String
"Type level variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
tn))))
             else () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    tyIs Name
con Type
t | (P NameType
_ Name
n' Type
_, [Type]
_) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
t
        = if Name
n' Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
tn then TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Name -> Maybe Type -> Err -> Err
forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating String
"constructor " Name
con Maybe Type
forall a. Maybe a
Nothing (String -> Err
forall t. String -> Err' t
Msg (Name -> String
forall a. Show a => a -> String
show Name
n' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
tn))))
             else () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    tyIs Name
con Type
t = TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Name -> Maybe Type -> Err -> Err
forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating String
"constructor " Name
con Maybe Type
forall a. Maybe a
Nothing (String -> Err
forall t. String -> Err' t
Msg (Type -> String
forall a. Show a => a -> String
show Type
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
tn))))

    mkLazy :: PTerm -> PTerm
mkLazy (PPi Plicity
pl Name
n FC
nfc PTerm
ty PTerm
sc)
        = let ty' :: PTerm
ty' = if PTerm -> Bool
getTyName PTerm
ty
                       then FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN String
"Delayed"))
                            [PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN String
"Infinite")),
                             PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
ty]
                       else PTerm
ty in
              Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
pl Name
n FC
nfc PTerm
ty' (PTerm -> PTerm
mkLazy PTerm
sc)
    mkLazy PTerm
t = PTerm
t

    getTyName :: PTerm -> Bool
getTyName (PApp FC
_ (PRef FC
_ [FC]
_ Name
n) [PArg]
_) = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Name
nsroot Name
tn
    getTyName (PRef FC
_ [FC]
_ Name
n) = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Name
nsroot Name
tn
    getTyName PTerm
_ = Bool
False

    -- if the constructor is a UniqueType, the datatype must be too
    -- (AnyType is fine, since that is checked for uniqueness too)
    -- if hte contructor is AnyType, the datatype must be at least AnyType
    checkUniqueKind :: TT n -> TT n -> Idris ()
checkUniqueKind (UType Universe
NullType) (UType Universe
NullType) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    checkUniqueKind (UType Universe
NullType) TT n
_
        = TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Universe -> Name -> Err
forall t. Universe -> Name -> Err' t
UniqueKindError Universe
NullType Name
n))
    checkUniqueKind (UType Universe
UniqueType) (UType Universe
UniqueType) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    checkUniqueKind (UType Universe
UniqueType) (UType Universe
AllTypes) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    checkUniqueKind (UType Universe
UniqueType) TT n
_
        = TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Universe -> Name -> Err
forall t. Universe -> Name -> Err' t
UniqueKindError Universe
UniqueType Name
n))
    checkUniqueKind (UType Universe
AllTypes) (UType Universe
AllTypes) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    checkUniqueKind (UType Universe
AllTypes) (UType Universe
UniqueType) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    checkUniqueKind (UType Universe
AllTypes) TT n
_
        = TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Universe -> Name -> Err
forall t. Universe -> Name -> Err' t
UniqueKindError Universe
AllTypes Name
n))
    checkUniqueKind TT n
_ TT n
_ = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

forceArgs :: Context -> Name -> Type -> [Int]
forceArgs :: Context -> Name -> Type -> [Int]
forceArgs Context
ctxt Name
tn Type
ty = Int -> Type -> [Int]
forceFrom Int
0 Type
ty
  where
    -- for each argument, substitute in MN pos "FF"
    -- then when we look at the return type, if we see MN pos name
    -- constructor guarded, then 'pos' is a forceable position
    forceFrom :: Int -> Type -> [Int]
    forceFrom :: Int -> Type -> [Int]
forceFrom Int
i (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
_ Type
_) Type
sc)
       = Int -> Type -> [Int]
forceFrom (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (Int -> String -> Name
sMN Int
i String
"FF") Type
forall n. TT n
Erased) Type
sc)
    forceFrom Int
i Type
sc
        -- Go under the top level type application
        -- We risk affecting erasure of more complex indices, so we'll only
        -- mark something forced if *everything* which appears in an index
        -- is forceable
        -- (FIXME: Actually the real risk is if we erase something a programmer
        -- definitely wants, which is particularly the case with 'views'.
        -- So perhaps we need a way of marking that in the source?)
        | (P NameType
_ Name
ty Type
_, [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
sc,
          Name
ty Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
tn -- Must be the right top level type!
             = if [Int] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((Type -> [Int]) -> [Type] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Bool -> Type -> [Int]
findNonForcePos Bool
True) [Type]
args)
                  then [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub ((Type -> [Int]) -> [Type] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Int]
findForcePos [Type]
args)
                  else []
    forceFrom Int
i Type
sc = []

    findForcePos :: Type -> [Int]
findForcePos (P NameType
_ (MN Int
i Text
ff) Type
_)
        | Text
ff Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"FF" = [Int
i]
    -- Only look under constructors in applications
    findForcePos ap :: Type
ap@(App AppStatus Name
_ Type
f Type
a)
        | (P NameType
_ Name
con Type
_, [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap,
          Name -> Context -> Bool
isDConName Name
con Context
ctxt
            = [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ (Type -> [Int]) -> [Type] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Int]
findForcePos [Type]
args
    findForcePos Type
_ = []

    findNonForcePos :: Bool -> Type -> [Int]
findNonForcePos Bool
fok (P NameType
_ (MN Int
i Text
ff) Type
_)
        | Text
ff Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"FF" = if Bool
fok then [] else [Int
i]
    -- Look under non-constructors in applications for things which can't
    -- be forced
    findNonForcePos Bool
fok ap :: Type
ap@(App AppStatus Name
_ Type
f Type
a)
        | (P NameType
_ Name
con Type
_, [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap
            = [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ (Type -> [Int]) -> [Type] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Bool -> Type -> [Int]
findNonForcePos (Bool
fok Bool -> Bool -> Bool
&& Name -> Context -> Bool
isConName Name
con Context
ctxt)) [Type]
args
    findNonForcePos Bool
_ Type
_ = []

addParamConstraints :: FC -> [Int] -> Type -> [(Name, Type)] -> Idris ()
addParamConstraints :: FC -> [Int] -> Type -> [(Name, Type)] -> Idris ()
addParamConstraints FC
fc [Int]
ps Type
cty [(Name, Type)]
cons
   = case Type -> Type
forall n. TT n -> TT n
getRetTy Type
cty of
          TType UExp
cvar -> ((Type, [Name]) -> Idris ()) -> [(Type, [Name])] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Int] -> UExp -> (Type, [Name]) -> Idris ()
forall {t :: * -> *} {n} {p}.
(Foldable t, Eq n) =>
p -> UExp -> (TT n, t n) -> Idris ()
addConConstraint [Int]
ps UExp
cvar)
                              (((Name, Type) -> (Type, [Name]))
-> [(Name, Type)] -> [(Type, [Name])]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> (Type, [Name])
forall {a} {a}. (a, TT a) -> (TT a, [a])
getParamNames [(Name, Type)]
cons)
          Type
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    getParamNames :: (a, TT a) -> (TT a, [a])
getParamNames (a
n, TT a
ty) = (TT a
ty, TT a -> [a]
forall {a}. TT a -> [a]
getPs TT a
ty)

    getPs :: TT a -> [a]
getPs (Bind a
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT a
_ TT a
_) TT a
sc)
       = TT a -> [a]
getPs (TT a -> TT a -> TT a
forall n. TT n -> TT n -> TT n
substV (NameType -> a -> TT a -> TT a
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref a
n TT a
forall n. TT n
Erased) TT a
sc)
    getPs TT a
t | (TT a
f, [TT a]
args) <- TT a -> (TT a, [TT a])
forall n. TT n -> (TT n, [TT n])
unApply TT a
t
       = Int -> [TT a] -> [a]
forall {a}. Int -> [TT a] -> [a]
paramArgs Int
0 [TT a]
args

    paramArgs :: Int -> [TT a] -> [a]
paramArgs Int
i (P NameType
_ a
n TT a
_ : [TT a]
args) | Int
i Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
ps = a
n a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Int -> [TT a] -> [a]
paramArgs (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [TT a]
args
    paramArgs Int
i (TT a
_ : [TT a]
args) = Int -> [TT a] -> [a]
paramArgs (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [TT a]
args
    paramArgs Int
i [] = []

    addConConstraint :: p -> UExp -> (TT n, t n) -> Idris ()
addConConstraint p
ps UExp
cvar (TT n
ty, t n
pnames) = TT n -> Idris ()
constraintTy TT n
ty
      where
        constraintTy :: TT n -> Idris ()
constraintTy (Bind n
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT n
ty TT n
_) TT n
sc)
           = case TT n -> TT n
forall n. TT n -> TT n
getRetTy TT n
ty of
                  TType UExp
avar -> do Bool
tit <- Idris Bool
typeInType
                                   Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
tit) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
                                       Context
ctxt <- Idris Context
getContext
                                       let tv :: Int
tv = Context -> Int
next_tvar Context
ctxt
                                       let con :: UConstraint
con = if n
n n -> t n -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t n
pnames
                                                    then UExp -> UExp -> UConstraint
ULE UExp
avar UExp
cvar
                                                    else UExp -> UExp -> UConstraint
ULT UExp
avar UExp
cvar
                                       FC -> (Int, [UConstraint]) -> Idris ()
addConstraints FC
fc (Int
tv, [UConstraint
con])
                                       IBCWrite -> Idris ()
addIBC (FC -> UConstraint -> IBCWrite
IBCConstraint FC
fc UConstraint
con)
                  TT n
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        constraintTy TT n
t = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()