{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Infer
( checkE
, checkSigB
, inferModule
, inferBinds
, checkTopDecls
)
where
import Data.Text(Text)
import qualified Data.Text as Text
import Cryptol.ModuleSystem.Name (lookupPrimDecl,nameLoc)
import Cryptol.Parser.Position
import qualified Cryptol.Parser.AST as P
import qualified Cryptol.ModuleSystem.Exports as P
import Cryptol.TypeCheck.AST hiding (tSub,tMul,tExp)
import Cryptol.TypeCheck.Monad
import Cryptol.TypeCheck.Error
import Cryptol.TypeCheck.Solve
import Cryptol.TypeCheck.SimpType(tMul)
import Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
checkPropSyn,checkNewtype,
checkParameterType,
checkPrimType,
checkParameterConstraints)
import Cryptol.TypeCheck.Instantiate
import Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),isEmptySubst)
import Cryptol.Utils.Ident
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.RecordMap
import qualified Data.Map as Map
import Data.Map (Map)
import qualified Data.Set as Set
import Data.List(foldl',sortBy,groupBy)
import Data.Either(partitionEithers)
import Data.Maybe(isJust, fromMaybe, mapMaybe)
import Data.List(partition)
import Data.Ratio(numerator,denominator)
import Data.Traversable(forM)
import Data.Function(on)
import Control.Monad(zipWithM,unless,foldM,forM_)
inferModule :: P.Module Name -> InferM Module
inferModule :: Module Name -> InferM Module
inferModule Module Name
m =
do ModName -> [Import] -> ExportSpec Name -> InferM ()
newModuleScope (Located ModName -> ModName
forall a. Located a -> a
thing (Module Name -> Located ModName
forall mname name. ModuleG mname name -> Located mname
P.mName Module Name
m)) ((Located Import -> Import) -> [Located Import] -> [Import]
forall a b. (a -> b) -> [a] -> [b]
map Located Import -> Import
forall a. Located a -> a
thing (Module Name -> [Located Import]
forall mname name. ModuleG mname name -> [Located Import]
P.mImports Module Name
m))
(Module Name -> ExportSpec Name
forall name mname.
Ord name =>
ModuleG mname name -> ExportSpec name
P.modExports Module Name
m)
[TopDecl Name] -> InferM ()
checkTopDecls (Module Name -> [TopDecl Name]
forall mname name. ModuleG mname name -> [TopDecl name]
P.mDecls Module Name
m)
InferM ()
proveModuleTopLevel
InferM Module
endModule
mkPrim :: String -> InferM (P.Expr Name)
mkPrim :: String -> InferM (Expr Name)
mkPrim String
str =
do Name
nm <- String -> InferM Name
mkPrim' String
str
Expr Name -> InferM (Expr Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Expr Name
forall n. n -> Expr n
P.EVar Name
nm)
mkPrim' :: String -> InferM Name
mkPrim' :: String -> InferM Name
mkPrim' String
str =
do PrimMap
prims <- InferM PrimMap
getPrimMap
Name -> InferM Name
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimIdent -> PrimMap -> Name
lookupPrimDecl (Text -> PrimIdent
prelPrim (String -> Text
Text.pack String
str)) PrimMap
prims)
desugarLiteral :: P.Literal -> InferM (P.Expr Name)
desugarLiteral :: Literal -> InferM (Expr Name)
desugarLiteral Literal
lit =
do Range
l <- InferM Range
curRange
Expr Name
numberPrim <- String -> InferM (Expr Name)
mkPrim String
"number"
Expr Name
fracPrim <- String -> InferM (Expr Name)
mkPrim String
"fraction"
let named :: (String, Type name) -> TypeInst name
named (String
x,Type name
y) = Named (Type name) -> TypeInst name
forall name. Named (Type name) -> TypeInst name
P.NamedInst
Named :: forall a. Located Ident -> a -> Named a
P.Named { name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type name
value = Type name
y }
number :: [(String, Type Name)] -> Expr Name
number [(String, Type Name)]
fs = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
numberPrim (((String, Type Name) -> TypeInst Name)
-> [(String, Type Name)] -> [TypeInst Name]
forall a b. (a -> b) -> [a] -> [b]
map (String, Type Name) -> TypeInst Name
forall name. (String, Type name) -> TypeInst name
named [(String, Type Name)]
fs)
tBits :: Integer -> Type n
tBits Integer
n = Type n -> Type n -> Type n
forall n. Type n -> Type n -> Type n
P.TSeq (Integer -> Type n
forall n. Integer -> Type n
P.TNum Integer
n) Type n
forall n. Type n
P.TBit
Expr Name -> InferM (Expr Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr Name -> InferM (Expr Name))
-> Expr Name -> InferM (Expr Name)
forall a b. (a -> b) -> a -> b
$ case Literal
lit of
P.ECNum Integer
num NumInfo
info ->
[(String, Type Name)] -> Expr Name
number ([(String, Type Name)] -> Expr Name)
-> [(String, Type Name)] -> Expr Name
forall a b. (a -> b) -> a -> b
$ [ (String
"val", Integer -> Type Name
forall n. Integer -> Type n
P.TNum Integer
num) ] [(String, Type Name)]
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. [a] -> [a] -> [a]
++ case NumInfo
info of
P.BinLit Text
_ Int
n -> [ (String
"rep", Integer -> Type Name
forall n. Integer -> Type n
tBits (Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)) ]
P.OctLit Text
_ Int
n -> [ (String
"rep", Integer -> Type Name
forall n. Integer -> Type n
tBits (Integer
3 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)) ]
P.HexLit Text
_ Int
n -> [ (String
"rep", Integer -> Type Name
forall n. Integer -> Type n
tBits (Integer
4 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)) ]
P.DecLit Text
_ -> [ ]
P.PolyLit Int
_n -> [ (String
"rep", Type Name -> Type Name -> Type Name
forall n. Type n -> Type n -> Type n
P.TSeq Type Name
forall n. Type n
P.TWild Type Name
forall n. Type n
P.TBit) ]
P.ECFrac Rational
fr FracInfo
info ->
let arg :: (Rational -> Integer) -> TypeInst name
arg Rational -> Integer
f = Type name -> TypeInst name
forall name. Type name -> TypeInst name
P.PosInst (Integer -> Type name
forall n. Integer -> Type n
P.TNum (Rational -> Integer
f Rational
fr))
rnd :: TypeInst name
rnd = Type name -> TypeInst name
forall name. Type name -> TypeInst name
P.PosInst (Integer -> Type name
forall n. Integer -> Type n
P.TNum (case FracInfo
info of
P.DecFrac Text
_ -> Integer
0
P.BinFrac Text
_ -> Integer
1
P.OctFrac Text
_ -> Integer
1
P.HexFrac Text
_ -> Integer
1))
in Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
fracPrim [ (Rational -> Integer) -> TypeInst Name
forall name. (Rational -> Integer) -> TypeInst name
arg Rational -> Integer
forall a. Ratio a -> a
numerator, (Rational -> Integer) -> TypeInst Name
forall name. (Rational -> Integer) -> TypeInst name
arg Rational -> Integer
forall a. Ratio a -> a
denominator, TypeInst Name
forall name. TypeInst name
rnd ]
P.ECChar Char
c ->
[(String, Type Name)] -> Expr Name
number [ (String
"val", Integer -> Type Name
forall n. Integer -> Type n
P.TNum (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c)))
, (String
"rep", Integer -> Type Name
forall n. Integer -> Type n
tBits (Integer
8 :: Integer)) ]
P.ECString String
s ->
Expr Name -> Type Name -> Expr Name
forall n. Expr n -> Type n -> Expr n
P.ETyped ([Expr Name] -> Expr Name
forall n. [Expr n] -> Expr n
P.EList [ Literal -> Expr Name
forall n. Literal -> Expr n
P.ELit (Char -> Literal
P.ECChar Char
c) | Char
c <- String
s ])
(Type Name -> Type Name -> Type Name
forall n. Type n -> Type n -> Type n
P.TSeq Type Name
forall n. Type n
P.TWild (Type Name -> Type Name -> Type Name
forall n. Type n -> Type n -> Type n
P.TSeq (Integer -> Type Name
forall n. Integer -> Type n
P.TNum Integer
8) Type Name
forall n. Type n
P.TBit))
appTys :: P.Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys :: Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
expr [TypeArg]
ts TypeWithSource
tGoal =
case Expr Name
expr of
P.EVar Name
x ->
do VarType
res <- Name -> InferM VarType
lookupVar Name
x
(Expr
e',Type
t) <- case VarType
res of
ExtVar Schema
s -> Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Type)
instantiateWith Name
x (Name -> Expr
EVar Name
x) Schema
s [TypeArg]
ts
CurSCC Expr
e Type
t -> do [TypeArg] -> InferM ()
checkNoParams [TypeArg]
ts
(Expr, Type) -> InferM (Expr, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e,Type
t)
Type -> TypeWithSource -> InferM ()
checkHasType Type
t TypeWithSource
tGoal
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'
P.ELit Literal
l -> do Expr Name
e <- Literal -> InferM (Expr Name)
desugarLiteral Literal
l
Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e [TypeArg]
ts TypeWithSource
tGoal
P.EAppT Expr Name
e [TypeInst Name]
fs -> Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e ((TypeInst Name -> TypeArg) -> [TypeInst Name] -> [TypeArg]
forall a b. (a -> b) -> [a] -> [b]
map TypeInst Name -> TypeArg
uncheckedTypeArg [TypeInst Name]
fs [TypeArg] -> [TypeArg] -> [TypeArg]
forall a. [a] -> [a] -> [a]
++ [TypeArg]
ts) TypeWithSource
tGoal
P.EWhere Expr Name
e [Decl Name]
ds ->
do (Expr
e1,[DeclGroup]
ds1) <- [Decl Name] -> InferM Expr -> InferM (Expr, [DeclGroup])
forall a. [Decl Name] -> InferM a -> InferM (a, [DeclGroup])
checkLocalDecls [Decl Name]
ds (Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e [TypeArg]
ts TypeWithSource
tGoal)
Expr -> InferM Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> [DeclGroup] -> Expr
EWhere Expr
e1 [DeclGroup]
ds1)
P.ELocated Expr Name
e Range
r ->
do Expr
e' <- Range -> InferM Expr -> InferM Expr
forall a. Range -> InferM a -> InferM a
inRange Range
r (Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e [TypeArg]
ts TypeWithSource
tGoal)
Bool
cs <- InferM Bool
getCallStacks
if Bool
cs then Expr -> InferM Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Range -> Expr -> Expr
ELocated Range
r Expr
e') else Expr -> InferM Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e'
P.ENeg {} -> InferM Expr
mono
P.EComplement {} -> InferM Expr
mono
P.EGenerate {} -> InferM Expr
mono
P.ETuple {} -> InferM Expr
mono
P.ERecord {} -> InferM Expr
mono
P.EUpd {} -> InferM Expr
mono
P.ESel {} -> InferM Expr
mono
P.EList {} -> InferM Expr
mono
P.EFromTo {} -> InferM Expr
mono
P.EFromToBy {} -> InferM Expr
mono
P.EFromToDownBy {} -> InferM Expr
mono
P.EFromToLessThan {} -> InferM Expr
mono
P.EInfFrom {} -> InferM Expr
mono
P.EComp {} -> InferM Expr
mono
P.EApp {} -> InferM Expr
mono
P.EIf {} -> InferM Expr
mono
P.ETyped {} -> InferM Expr
mono
P.ETypeVal {} -> InferM Expr
mono
P.EFun {} -> InferM Expr
mono
P.ESplit {} -> InferM Expr
mono
P.EParens Expr Name
e -> Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e [TypeArg]
ts TypeWithSource
tGoal
P.EInfix Expr Name
a Located Name
op Fixity
_ Expr Name
b -> Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys (Name -> Expr Name
forall n. n -> Expr n
P.EVar (Located Name -> Name
forall a. Located a -> a
thing Located Name
op) Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
a Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
b) [TypeArg]
ts TypeWithSource
tGoal
where mono :: InferM Expr
mono = do Expr
e' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
expr TypeWithSource
tGoal
[TypeArg] -> InferM ()
checkNoParams [TypeArg]
ts
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'
checkNoParams :: [TypeArg] -> InferM ()
checkNoParams :: [TypeArg] -> InferM ()
checkNoParams [TypeArg]
ts =
case [TypeArg]
pos of
TypeArg
p : [TypeArg]
_ -> do Range
r <- case TypeArg -> MaybeCheckedType
tyArgType TypeArg
p of
Unchecked Type Name
t | Just Range
r <- Type Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Type Name
t -> Range -> InferM Range
forall (f :: * -> *) a. Applicative f => a -> f a
pure Range
r
MaybeCheckedType
_ -> InferM Range
curRange
Range -> InferM () -> InferM ()
forall a. Range -> InferM a -> InferM a
inRange Range
r (Error -> InferM ()
recordError Error
TooManyPositionalTypeParams)
[TypeArg]
_ -> (TypeArg -> InferM ()) -> [TypeArg] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TypeArg -> InferM ()
badNamed [TypeArg]
named
where
badNamed :: TypeArg -> InferM ()
badNamed TypeArg
l =
case TypeArg -> Maybe (Located Ident)
tyArgName TypeArg
l of
Just Located Ident
i -> Error -> InferM ()
recordError (Located Ident -> Error
UndefinedTypeParameter Located Ident
i)
Maybe (Located Ident)
Nothing -> () -> InferM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
([TypeArg]
named,[TypeArg]
pos) = (TypeArg -> Bool) -> [TypeArg] -> ([TypeArg], [TypeArg])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Maybe (Located Ident) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Located Ident) -> Bool)
-> (TypeArg -> Maybe (Located Ident)) -> TypeArg -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeArg -> Maybe (Located Ident)
tyArgName) [TypeArg]
ts
checkTypeOfKind :: P.Type Name -> Kind -> InferM Type
checkTypeOfKind :: Type Name -> Kind -> InferM Type
checkTypeOfKind Type Name
ty Kind
k = Type Name -> Maybe Kind -> InferM Type
checkType Type Name
ty (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
k)
checkE :: P.Expr Name -> TypeWithSource -> InferM Expr
checkE :: Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
expr TypeWithSource
tGoal =
case Expr Name
expr of
P.EVar Name
x ->
do VarType
res <- Name -> InferM VarType
lookupVar Name
x
(Expr
e',Type
t) <- case VarType
res of
ExtVar Schema
s -> Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Type)
instantiateWith Name
x (Name -> Expr
EVar Name
x) Schema
s []
CurSCC Expr
e Type
t -> (Expr, Type) -> InferM (Expr, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Type
t)
Type -> TypeWithSource -> InferM ()
checkHasType Type
t TypeWithSource
tGoal
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'
P.ENeg Expr Name
e ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"negate"
Expr Name -> TypeWithSource -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e) TypeWithSource
tGoal
P.EComplement Expr Name
e ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"complement"
Expr Name -> TypeWithSource -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e) TypeWithSource
tGoal
P.EGenerate Expr Name
e ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"generate"
Expr Name -> TypeWithSource -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e) TypeWithSource
tGoal
P.ELit l :: Literal
l@(P.ECNum Integer
_ (P.DecLit Text
_)) ->
do Expr Name
e <- Literal -> InferM (Expr Name)
desugarLiteral Literal
l
Range
loc <- InferM Range
curRange
let arg :: TypeArg
arg = TypeArg :: Maybe (Located Ident) -> MaybeCheckedType -> TypeArg
TypeArg { tyArgName :: Maybe (Located Ident)
tyArgName = Located Ident -> Maybe (Located Ident)
forall a. a -> Maybe a
Just (Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
loc (String -> Ident
packIdent String
"rep"))
, tyArgType :: MaybeCheckedType
tyArgType = Type -> MaybeCheckedType
Checked (TypeWithSource -> Type
twsType TypeWithSource
tGoal)
}
Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e [TypeArg
arg] TypeWithSource
tGoal
P.ELit Literal
l -> (Expr Name -> TypeWithSource -> InferM Expr
`checkE` TypeWithSource
tGoal) (Expr Name -> InferM Expr) -> InferM (Expr Name) -> InferM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Literal -> InferM (Expr Name)
desugarLiteral Literal
l
P.ETuple [Expr Name]
es ->
do [Type]
etys <- Int -> TypeWithSource -> InferM [Type]
expectTuple ([Expr Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr Name]
es) TypeWithSource
tGoal
let mkTGoal :: Int -> Type -> TypeWithSource
mkTGoal Int
n Type
t = Type -> TypeSource -> TypeWithSource
WithSource Type
t (Int -> TypeSource
TypeOfTupleField Int
n)
[Expr]
es' <- (Expr Name -> TypeWithSource -> InferM Expr)
-> [Expr Name] -> [TypeWithSource] -> InferM [Expr]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Expr Name -> TypeWithSource -> InferM Expr
checkE [Expr Name]
es ((Int -> Type -> TypeWithSource)
-> [Int] -> [Type] -> [TypeWithSource]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Type -> TypeWithSource
mkTGoal [Int
1..] [Type]
etys)
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Expr
ETuple [Expr]
es')
P.ERecord Rec (Expr Name)
fs ->
do RecordMap Ident (Expr Name, Type)
es <- Rec (Expr Name)
-> TypeWithSource -> InferM (RecordMap Ident (Expr Name, Type))
forall a.
RecordMap Ident (Range, a)
-> TypeWithSource -> InferM (RecordMap Ident (a, Type))
expectRec Rec (Expr Name)
fs TypeWithSource
tGoal
let checkField :: Ident -> (Expr Name, Type) -> InferM Expr
checkField Ident
f (Expr Name
e,Type
t) = Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Type -> TypeSource -> TypeWithSource
WithSource Type
t (Ident -> TypeSource
TypeOfRecordField Ident
f))
RecordMap Ident Expr
es' <- (Ident -> (Expr Name, Type) -> InferM Expr)
-> RecordMap Ident (Expr Name, Type)
-> InferM (RecordMap Ident Expr)
forall (t :: * -> *) a b c.
Applicative t =>
(a -> b -> t c) -> RecordMap a b -> t (RecordMap a c)
traverseRecordMap Ident -> (Expr Name, Type) -> InferM Expr
checkField RecordMap Ident (Expr Name, Type)
es
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (RecordMap Ident Expr -> Expr
ERec RecordMap Ident Expr
es')
P.EUpd Maybe (Expr Name)
x [UpdField Name]
fs -> Maybe (Expr Name)
-> [UpdField Name] -> TypeWithSource -> InferM Expr
checkRecUpd Maybe (Expr Name)
x [UpdField Name]
fs TypeWithSource
tGoal
P.ESel Expr Name
e Selector
l ->
do let src :: TypeSource
src = Selector -> TypeSource
selSrc Selector
l
Type
t <- TypeSource -> Kind -> InferM Type
newType TypeSource
src Kind
KType
Expr
e' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Type -> TypeSource -> TypeWithSource
WithSource Type
t TypeSource
src)
HasGoalSln
f <- Selector -> Type -> Type -> InferM HasGoalSln
newHasGoal Selector
l Type
t (TypeWithSource -> Type
twsType TypeWithSource
tGoal)
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (HasGoalSln -> Expr -> Expr
hasDoSelect HasGoalSln
f Expr
e')
P.EList [] ->
do (Type
len,Type
a) <- TypeWithSource -> InferM (Type, Type)
expectSeq TypeWithSource
tGoal
Int -> TypeWithSource -> InferM ()
expectFin Int
0 (Type -> TypeSource -> TypeWithSource
WithSource Type
len TypeSource
LenOfSeq)
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Type -> Expr
EList [] Type
a)
P.EList [Expr Name]
es ->
do (Type
len,Type
a) <- TypeWithSource -> InferM (Type, Type)
expectSeq TypeWithSource
tGoal
Int -> TypeWithSource -> InferM ()
expectFin ([Expr Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr Name]
es) (Type -> TypeSource -> TypeWithSource
WithSource Type
len TypeSource
LenOfSeq)
let checkElem :: Expr Name -> InferM Expr
checkElem Expr Name
e = Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Type -> TypeSource -> TypeWithSource
WithSource Type
a TypeSource
TypeOfSeqElement)
[Expr]
es' <- (Expr Name -> InferM Expr) -> [Expr Name] -> InferM [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Expr Name -> InferM Expr
checkElem [Expr Name]
es
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Type -> Expr
EList [Expr]
es' Type
a)
P.EFromToBy Bool
isStrict Type Name
t1 Type Name
t2 Type Name
t3 Maybe (Type Name)
mety
| Bool
isStrict ->
do Range
l <- InferM Range
curRange
let fs :: [(String, Type Name)]
fs = [(String
"first",Type Name
t1),(String
"bound",Type Name
t2),(String
"stride",Type Name
t3)] [(String, Type Name)]
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. [a] -> [a] -> [a]
++
case Maybe (Type Name)
mety of
Just Type Name
ety -> [(String
"a",Type Name
ety)]
Maybe (Type Name)
Nothing -> []
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"fromToByLessThan"
let e' :: Expr Name
e' = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[ Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst Named :: forall a. Located Ident -> a -> Named a
P.Named{ name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
| (String
x,Type Name
y) <- [(String, Type Name)]
fs
]
Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal
| Bool
otherwise ->
do Range
l <- InferM Range
curRange
let fs :: [(String, Type Name)]
fs = [(String
"first",Type Name
t1),(String
"last",Type Name
t2),(String
"stride",Type Name
t3)] [(String, Type Name)]
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. [a] -> [a] -> [a]
++
case Maybe (Type Name)
mety of
Just Type Name
ety -> [(String
"a",Type Name
ety)]
Maybe (Type Name)
Nothing -> []
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"fromToBy"
let e' :: Expr Name
e' = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[ Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst Named :: forall a. Located Ident -> a -> Named a
P.Named{ name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
| (String
x,Type Name
y) <- [(String, Type Name)]
fs
]
Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal
P.EFromToDownBy Bool
isStrict Type Name
t1 Type Name
t2 Type Name
t3 Maybe (Type Name)
mety
| Bool
isStrict ->
do Range
l <- InferM Range
curRange
let fs :: [(String, Type Name)]
fs = [(String
"first",Type Name
t1),(String
"bound",Type Name
t2),(String
"stride",Type Name
t3)] [(String, Type Name)]
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. [a] -> [a] -> [a]
++
case Maybe (Type Name)
mety of
Just Type Name
ety -> [(String
"a",Type Name
ety)]
Maybe (Type Name)
Nothing -> []
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"fromToDownByGreaterThan"
let e' :: Expr Name
e' = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[ Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst Named :: forall a. Located Ident -> a -> Named a
P.Named{ name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
| (String
x,Type Name
y) <- [(String, Type Name)]
fs
]
Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal
| Bool
otherwise ->
do Range
l <- InferM Range
curRange
let fs :: [(String, Type Name)]
fs = [(String
"first",Type Name
t1),(String
"last",Type Name
t2),(String
"stride",Type Name
t3)] [(String, Type Name)]
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. [a] -> [a] -> [a]
++
case Maybe (Type Name)
mety of
Just Type Name
ety -> [(String
"a",Type Name
ety)]
Maybe (Type Name)
Nothing -> []
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"fromToDownBy"
let e' :: Expr Name
e' = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[ Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst Named :: forall a. Located Ident -> a -> Named a
P.Named{ name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
| (String
x,Type Name
y) <- [(String, Type Name)]
fs
]
Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal
P.EFromToLessThan Type Name
t1 Type Name
t2 Maybe (Type Name)
mety ->
do Range
l <- InferM Range
curRange
let fs0 :: [(String, Type Name)]
fs0 =
case Maybe (Type Name)
mety of
Just Type Name
ety -> [(String
"a", Type Name
ety)]
Maybe (Type Name)
Nothing -> []
let fs :: [(String, Type Name)]
fs = [(String
"first", Type Name
t1), (String
"bound", Type Name
t2)] [(String, Type Name)]
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. [a] -> [a] -> [a]
++ [(String, Type Name)]
fs0
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"fromToLessThan"
let e' :: Expr Name
e' = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[ Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst Named :: forall a. Located Ident -> a -> Named a
P.Named { name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
| (String
x,Type Name
y) <- [(String, Type Name)]
fs
]
Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal
P.EFromTo Type Name
t1 Maybe (Type Name)
mbt2 Type Name
t3 Maybe (Type Name)
mety ->
do Range
l <- InferM Range
curRange
let fs0 :: [(String, Type Name)]
fs0 =
case Maybe (Type Name)
mety of
Just Type Name
ety -> [(String
"a", Type Name
ety)]
Maybe (Type Name)
Nothing -> []
let (String
c,[(String, Type Name)]
fs) =
case Maybe (Type Name)
mbt2 of
Maybe (Type Name)
Nothing ->
(String
"fromTo", (String
"last", Type Name
t3) (String, Type Name)
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. a -> [a] -> [a]
: [(String, Type Name)]
fs0)
Just Type Name
t2 ->
(String
"fromThenTo", (String
"next",Type Name
t2) (String, Type Name)
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. a -> [a] -> [a]
: (String
"last",Type Name
t3) (String, Type Name)
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. a -> [a] -> [a]
: [(String, Type Name)]
fs0)
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
c
let e' :: Expr Name
e' = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[ Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst Named :: forall a. Located Ident -> a -> Named a
P.Named { name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
| (String
x,Type Name
y) <- (String
"first",Type Name
t1) (String, Type Name)
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. a -> [a] -> [a]
: [(String, Type Name)]
fs
]
Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal
P.EInfFrom Expr Name
e1 Maybe (Expr Name)
Nothing ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"infFrom"
Expr Name -> TypeWithSource -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e1) TypeWithSource
tGoal
P.EInfFrom Expr Name
e1 (Just Expr Name
e2) ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"infFromThen"
Expr Name -> TypeWithSource -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e1) Expr Name
e2) TypeWithSource
tGoal
P.EComp Expr Name
e [[Match Name]]
mss ->
do ([[Match]]
mss', [Map Name (Located Type)]
dss, [Type]
ts) <- [([Match], Map Name (Located Type), Type)]
-> ([[Match]], [Map Name (Located Type)], [Type])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 ([([Match], Map Name (Located Type), Type)]
-> ([[Match]], [Map Name (Located Type)], [Type]))
-> InferM [([Match], Map Name (Located Type), Type)]
-> InferM ([[Match]], [Map Name (Located Type)], [Type])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Int
-> [Match Name] -> InferM ([Match], Map Name (Located Type), Type))
-> [Int]
-> [[Match Name]]
-> InferM [([Match], Map Name (Located Type), Type)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Int
-> [Match Name] -> InferM ([Match], Map Name (Located Type), Type)
inferCArm [ Int
1 .. ] [[Match Name]]
mss
(Type
len,Type
a) <- TypeWithSource -> InferM (Type, Type)
expectSeq TypeWithSource
tGoal
Type
inferred <- [Type] -> InferM Type
smallest [Type]
ts
[Type]
ctrs <- TypeWithSource -> Type -> InferM [Type]
unify (Type -> TypeSource -> TypeWithSource
WithSource Type
len TypeSource
LenOfSeq) Type
inferred
ConstraintSource -> [Type] -> InferM ()
newGoals ConstraintSource
CtComprehension [Type]
ctrs
Map Name (Located Type)
ds <- [Map Name (Located Type)] -> InferM (Map Name (Located Type))
forall (m :: * -> *) a a.
(Monad m, Show a, Ord a) =>
[Map a (Located a)] -> m (Map a (Located a))
combineMaps [Map Name (Located Type)]
dss
Expr
e' <- Map Name (Located Type) -> InferM Expr -> InferM Expr
forall a. Map Name (Located Type) -> InferM a -> InferM a
withMonoTypes Map Name (Located Type)
ds (Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Type -> TypeSource -> TypeWithSource
WithSource Type
a TypeSource
TypeOfSeqElement))
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Expr -> [[Match]] -> Expr
EComp Type
len Type
a Expr
e' [[Match]]
mss')
where
combineMaps :: [Map a (Located a)] -> m (Map a (Located a))
combineMaps [Map a (Located a)]
ms = if [(a, [Range])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(a, [Range])]
bad
then Map a (Located a) -> m (Map a (Located a))
forall (m :: * -> *) a. Monad m => a -> m a
return ([Map a (Located a)] -> Map a (Located a)
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions [Map a (Located a)]
ms)
else String -> [String] -> m (Map a (Located a))
forall a. HasCallStack => String -> [String] -> a
panic String
"combineMaps" ([String] -> m (Map a (Located a)))
-> [String] -> m (Map a (Located a))
forall a b. (a -> b) -> a -> b
$ String
"Multiple definitions"
String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ((a, [Range]) -> String) -> [(a, [Range])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (a, [Range]) -> String
forall a. Show a => a -> String
show [(a, [Range])]
bad
where
bad :: [(a, [Range])]
bad = do Map a (Located a)
m <- [Map a (Located a)]
ms
[Located a] -> [(a, [Range])]
duplicates [ Located a
a { thing :: a
thing = a
x } | (a
x,Located a
a) <- Map a (Located a) -> [(a, Located a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map a (Located a)
m ]
duplicates :: [Located a] -> [(a, [Range])]
duplicates = ([Located a] -> Maybe (a, [Range]))
-> [[Located a]] -> [(a, [Range])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe [Located a] -> Maybe (a, [Range])
forall a. [Located a] -> Maybe (a, [Range])
multiple
([[Located a]] -> [(a, [Range])])
-> ([Located a] -> [[Located a]]) -> [Located a] -> [(a, [Range])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located a -> Located a -> Bool) -> [Located a] -> [[Located a]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==) (a -> a -> Bool)
-> (Located a -> a) -> Located a -> Located a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Located a -> a
forall a. Located a -> a
thing)
([Located a] -> [[Located a]])
-> ([Located a] -> [Located a]) -> [Located a] -> [[Located a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located a -> Located a -> Ordering) -> [Located a] -> [Located a]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (a -> a -> Ordering)
-> (Located a -> a) -> Located a -> Located a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Located a -> a
forall a. Located a -> a
thing)
where
multiple :: [Located a] -> Maybe (a, [Range])
multiple xs :: [Located a]
xs@(Located a
x : Located a
_ : [Located a]
_) = (a, [Range]) -> Maybe (a, [Range])
forall a. a -> Maybe a
Just (Located a -> a
forall a. Located a -> a
thing Located a
x, (Located a -> Range) -> [Located a] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map Located a -> Range
forall a. Located a -> Range
srcRange [Located a]
xs)
multiple [Located a]
_ = Maybe (a, [Range])
forall a. Maybe a
Nothing
P.EAppT Expr Name
e [TypeInst Name]
fs -> Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e ((TypeInst Name -> TypeArg) -> [TypeInst Name] -> [TypeArg]
forall a b. (a -> b) -> [a] -> [b]
map TypeInst Name -> TypeArg
uncheckedTypeArg [TypeInst Name]
fs) TypeWithSource
tGoal
P.EApp Expr Name
e1 Expr Name
e2 ->
do let argSrc :: TypeSource
argSrc = ArgDescr -> TypeSource
TypeOfArg ArgDescr
noArgDescr
Type
t1 <- TypeSource -> Kind -> InferM Type
newType TypeSource
argSrc Kind
KType
Expr
e1' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e1 (Type -> TypeSource -> TypeWithSource
WithSource (Type -> Type -> Type
tFun Type
t1 (TypeWithSource -> Type
twsType TypeWithSource
tGoal)) TypeSource
FunApp)
Expr
e2' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e2 (Type -> TypeSource -> TypeWithSource
WithSource Type
t1 TypeSource
argSrc)
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
EApp Expr
e1' Expr
e2')
P.EIf Expr Name
e1 Expr Name
e2 Expr Name
e3 ->
do Expr
e1' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e1 (Type -> TypeSource -> TypeWithSource
WithSource Type
tBit TypeSource
TypeOfIfCondExpr)
Expr
e2' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e2 TypeWithSource
tGoal
Expr
e3' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e3 TypeWithSource
tGoal
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr -> Expr
EIf Expr
e1' Expr
e2' Expr
e3')
P.EWhere Expr Name
e [Decl Name]
ds ->
do (Expr
e1,[DeclGroup]
ds1) <- [Decl Name] -> InferM Expr -> InferM (Expr, [DeclGroup])
forall a. [Decl Name] -> InferM a -> InferM (a, [DeclGroup])
checkLocalDecls [Decl Name]
ds (Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
tGoal)
Expr -> InferM Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> [DeclGroup] -> Expr
EWhere Expr
e1 [DeclGroup]
ds1)
P.ETyped Expr Name
e Type Name
t ->
do Type
tSig <- Type Name -> Kind -> InferM Type
checkTypeOfKind Type Name
t Kind
KType
Expr
e' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Type -> TypeSource -> TypeWithSource
WithSource Type
tSig TypeSource
TypeFromUserAnnotation)
Type -> TypeWithSource -> InferM ()
checkHasType Type
tSig TypeWithSource
tGoal
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'
P.ETypeVal Type Name
t ->
do Range
l <- InferM Range
curRange
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"number"
Expr Name -> TypeWithSource -> InferM Expr
checkE (Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst
Named :: forall a. Located Ident -> a -> Named a
P.Named { name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
"val")
, value :: Type Name
value = Type Name
t }]) TypeWithSource
tGoal
P.EFun FunDesc Name
desc [Pattern Name]
ps Expr Name
e -> FunDesc Name
-> [Pattern Name] -> Expr Name -> TypeWithSource -> InferM Expr
checkFun FunDesc Name
desc [Pattern Name]
ps Expr Name
e TypeWithSource
tGoal
P.ELocated Expr Name
e Range
r ->
do Expr
e' <- Range -> InferM Expr -> InferM Expr
forall a. Range -> InferM a -> InferM a
inRange Range
r (Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
tGoal)
Bool
cs <- InferM Bool
getCallStacks
if Bool
cs then Expr -> InferM Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Range -> Expr -> Expr
ELocated Range
r Expr
e') else Expr -> InferM Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e'
P.ESplit Expr Name
e ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"splitAt"
Expr Name -> TypeWithSource -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e) TypeWithSource
tGoal
P.EInfix Expr Name
a Located Name
op Fixity
_ Expr Name
b -> Expr Name -> TypeWithSource -> InferM Expr
checkE (Name -> Expr Name
forall n. n -> Expr n
P.EVar (Located Name -> Name
forall a. Located a -> a
thing Located Name
op) Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
a Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
b) TypeWithSource
tGoal
P.EParens Expr Name
e -> Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
tGoal
checkRecUpd ::
Maybe (P.Expr Name) -> [ P.UpdField Name ] -> TypeWithSource -> InferM Expr
checkRecUpd :: Maybe (Expr Name)
-> [UpdField Name] -> TypeWithSource -> InferM Expr
checkRecUpd Maybe (Expr Name)
mb [UpdField Name]
fs TypeWithSource
tGoal =
case Maybe (Expr Name)
mb of
Maybe (Expr Name)
Nothing ->
do Name
r <- Namespace -> Ident -> InferM Name
newParamName Namespace
NSValue (String -> Ident
packIdent String
"r")
let p :: Pattern Name
p = Located Name -> Pattern Name
forall n. Located n -> Pattern n
P.PVar Located :: forall a. Range -> a -> Located a
Located { srcRange :: Range
srcRange = Name -> Range
nameLoc Name
r, thing :: Name
thing = Name
r }
fe :: Expr Name
fe = FunDesc Name -> [Pattern Name] -> Expr Name -> Expr Name
forall n. FunDesc n -> [Pattern n] -> Expr n -> Expr n
P.EFun FunDesc Name
forall n. FunDesc n
P.emptyFunDesc [Pattern Name
p] (Maybe (Expr Name) -> [UpdField Name] -> Expr Name
forall n. Maybe (Expr n) -> [UpdField n] -> Expr n
P.EUpd (Expr Name -> Maybe (Expr Name)
forall a. a -> Maybe a
Just (Name -> Expr Name
forall n. n -> Expr n
P.EVar Name
r)) [UpdField Name]
fs)
Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
fe TypeWithSource
tGoal
Just Expr Name
e ->
do Expr
e1 <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
tGoal
(Expr -> UpdField Name -> InferM Expr)
-> Expr -> [UpdField Name] -> InferM Expr
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Expr -> UpdField Name -> InferM Expr
doUpd Expr
e1 [UpdField Name]
fs
where
doUpd :: Expr -> UpdField Name -> InferM Expr
doUpd Expr
e (P.UpdField UpdHow
how [Located Selector]
sels Expr Name
v) =
case [Located Selector]
sels of
[Located Selector
l] ->
case UpdHow
how of
UpdHow
P.UpdSet ->
do let src :: TypeSource
src = Selector -> TypeSource
selSrc Selector
s
Type
ft <- TypeSource -> Kind -> InferM Type
newType TypeSource
src Kind
KType
Expr
v1 <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
v (Type -> TypeSource -> TypeWithSource
WithSource Type
ft TypeSource
src)
HasGoalSln
d <- Selector -> Type -> Type -> InferM HasGoalSln
newHasGoal Selector
s (TypeWithSource -> Type
twsType TypeWithSource
tGoal) Type
ft
Expr -> InferM Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasGoalSln -> Expr -> Expr -> Expr
hasDoSet HasGoalSln
d Expr
e Expr
v1)
UpdHow
P.UpdFun ->
do let src :: TypeSource
src = Selector -> TypeSource
selSrc Selector
s
Type
ft <- TypeSource -> Kind -> InferM Type
newType TypeSource
src Kind
KType
Expr
v1 <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
v (Type -> TypeSource -> TypeWithSource
WithSource (Type -> Type -> Type
tFun Type
ft Type
ft) TypeSource
src)
HasGoalSln
d <- Selector -> Type -> Type -> InferM HasGoalSln
newHasGoal Selector
s (TypeWithSource -> Type
twsType TypeWithSource
tGoal) Type
ft
Name
tmp <- Namespace -> Ident -> InferM Name
newParamName Namespace
NSValue (String -> Ident
packIdent String
"rf")
let e' :: Expr
e' = Name -> Expr
EVar Name
tmp
Expr -> InferM Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> InferM Expr) -> Expr -> InferM Expr
forall a b. (a -> b) -> a -> b
$ HasGoalSln -> Expr -> Expr -> Expr
hasDoSet HasGoalSln
d Expr
e' (Expr -> Expr -> Expr
EApp Expr
v1 (HasGoalSln -> Expr -> Expr
hasDoSelect HasGoalSln
d Expr
e'))
Expr -> [DeclGroup] -> Expr
`EWhere`
[ Decl -> DeclGroup
NonRecursive
Decl :: Name
-> Schema
-> DeclDef
-> [Pragma]
-> Bool
-> Maybe Fixity
-> Maybe Text
-> Decl
Decl { dName :: Name
dName = Name
tmp
, dSignature :: Schema
dSignature = Type -> Schema
tMono (TypeWithSource -> Type
twsType TypeWithSource
tGoal)
, dDefinition :: DeclDef
dDefinition = Expr -> DeclDef
DExpr Expr
e
, dPragmas :: [Pragma]
dPragmas = []
, dInfix :: Bool
dInfix = Bool
False
, dFixity :: Maybe Fixity
dFixity = Maybe Fixity
forall a. Maybe a
Nothing
, dDoc :: Maybe Text
dDoc = Maybe Text
forall a. Maybe a
Nothing
} ]
where s :: Selector
s = Located Selector -> Selector
forall a. Located a -> a
thing Located Selector
l
[Located Selector]
_ -> String -> [String] -> InferM Expr
forall a. HasCallStack => String -> [String] -> a
panic String
"checkRecUpd/doUpd" [ String
"Expected exactly 1 field label"
, String
"Got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Located Selector] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Located Selector]
sels)
]
expectSeq :: TypeWithSource -> InferM (Type,Type)
expectSeq :: TypeWithSource -> InferM (Type, Type)
expectSeq tGoal :: TypeWithSource
tGoal@(WithSource Type
ty TypeSource
src) =
case Type
ty of
TUser Name
_ [Type]
_ Type
ty' ->
TypeWithSource -> InferM (Type, Type)
expectSeq (Type -> TypeSource -> TypeWithSource
WithSource Type
ty' TypeSource
src)
TCon (TC TC
TCSeq) [Type
a,Type
b] ->
(Type, Type) -> InferM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
a,Type
b)
TVar TVar
_ ->
do tys :: (Type, Type)
tys@(Type
a,Type
b) <- InferM (Type, Type)
genTys
ConstraintSource -> [Type] -> InferM ()
newGoals ConstraintSource
CtExactType ([Type] -> InferM ()) -> InferM [Type] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeWithSource -> Type -> InferM [Type]
unify TypeWithSource
tGoal (Type -> Type -> Type
tSeq Type
a Type
b)
(Type, Type) -> InferM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type, Type)
tys
Type
_ ->
do tys :: (Type, Type)
tys@(Type
a,Type
b) <- InferM (Type, Type)
genTys
Error -> InferM ()
recordError (TypeSource -> Type -> Type -> Error
TypeMismatch TypeSource
src Type
ty (Type -> Type -> Type
tSeq Type
a Type
b))
(Type, Type) -> InferM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type, Type)
tys
where
genTys :: InferM (Type, Type)
genTys =
do Type
a <- TypeSource -> Kind -> InferM Type
newType TypeSource
LenOfSeq Kind
KNum
Type
b <- TypeSource -> Kind -> InferM Type
newType TypeSource
TypeOfSeqElement Kind
KType
(Type, Type) -> InferM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
a,Type
b)
expectTuple :: Int -> TypeWithSource -> InferM [Type]
expectTuple :: Int -> TypeWithSource -> InferM [Type]
expectTuple Int
n tGoal :: TypeWithSource
tGoal@(WithSource Type
ty TypeSource
src) =
case Type
ty of
TUser Name
_ [Type]
_ Type
ty' ->
Int -> TypeWithSource -> InferM [Type]
expectTuple Int
n (Type -> TypeSource -> TypeWithSource
WithSource Type
ty' TypeSource
src)
TCon (TC (TCTuple Int
n')) [Type]
tys | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n' ->
[Type] -> InferM [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return [Type]
tys
TVar TVar
_ ->
do [Type]
tys <- InferM [Type]
genTys
ConstraintSource -> [Type] -> InferM ()
newGoals ConstraintSource
CtExactType ([Type] -> InferM ()) -> InferM [Type] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeWithSource -> Type -> InferM [Type]
unify TypeWithSource
tGoal ([Type] -> Type
tTuple [Type]
tys)
[Type] -> InferM [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return [Type]
tys
Type
_ ->
do [Type]
tys <- InferM [Type]
genTys
Error -> InferM ()
recordError (TypeSource -> Type -> Type -> Error
TypeMismatch TypeSource
src Type
ty ([Type] -> Type
tTuple [Type]
tys))
[Type] -> InferM [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return [Type]
tys
where
genTys :: InferM [Type]
genTys =[Int] -> (Int -> InferM Type) -> InferM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 ] ((Int -> InferM Type) -> InferM [Type])
-> (Int -> InferM Type) -> InferM [Type]
forall a b. (a -> b) -> a -> b
$ \ Int
i -> TypeSource -> Kind -> InferM Type
newType (Int -> TypeSource
TypeOfTupleField Int
i) Kind
KType
expectRec ::
RecordMap Ident (Range, a) ->
TypeWithSource ->
InferM (RecordMap Ident (a, Type))
expectRec :: RecordMap Ident (Range, a)
-> TypeWithSource -> InferM (RecordMap Ident (a, Type))
expectRec RecordMap Ident (Range, a)
fs tGoal :: TypeWithSource
tGoal@(WithSource Type
ty TypeSource
src) =
case Type
ty of
TUser Name
_ [Type]
_ Type
ty' ->
RecordMap Ident (Range, a)
-> TypeWithSource -> InferM (RecordMap Ident (a, Type))
forall a.
RecordMap Ident (Range, a)
-> TypeWithSource -> InferM (RecordMap Ident (a, Type))
expectRec RecordMap Ident (Range, a)
fs (Type -> TypeSource -> TypeWithSource
WithSource Type
ty' TypeSource
src)
TRec RecordMap Ident Type
ls
| Right RecordMap Ident (a, Type)
r <- (Ident -> (Range, a) -> Type -> (a, Type))
-> RecordMap Ident (Range, a)
-> RecordMap Ident Type
-> Either (Either Ident Ident) (RecordMap Ident (a, Type))
forall a b c d.
Ord a =>
(a -> b -> c -> d)
-> RecordMap a b
-> RecordMap a c
-> Either (Either a a) (RecordMap a d)
zipRecords (\Ident
_ (Range
_rng,a
v) Type
t -> (a
v,Type
t)) RecordMap Ident (Range, a)
fs RecordMap Ident Type
ls -> RecordMap Ident (a, Type) -> InferM (RecordMap Ident (a, Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure RecordMap Ident (a, Type)
r
Type
_ ->
do RecordMap Ident (a, Type)
res <- (Ident -> (Range, a) -> InferM (a, Type))
-> RecordMap Ident (Range, a) -> InferM (RecordMap Ident (a, Type))
forall (t :: * -> *) a b c.
Applicative t =>
(a -> b -> t c) -> RecordMap a b -> t (RecordMap a c)
traverseRecordMap
(\Ident
nm (Range
_rng,a
v) ->
do Type
t <- TypeSource -> Kind -> InferM Type
newType (Ident -> TypeSource
TypeOfRecordField Ident
nm) Kind
KType
(a, Type) -> InferM (a, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
v, Type
t))
RecordMap Ident (Range, a)
fs
let tys :: RecordMap Ident Type
tys = ((a, Type) -> Type)
-> RecordMap Ident (a, Type) -> RecordMap Ident Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, Type) -> Type
forall a b. (a, b) -> b
snd RecordMap Ident (a, Type)
res
case Type
ty of
TVar TVFree{} -> do [Type]
ps <- TypeWithSource -> Type -> InferM [Type]
unify TypeWithSource
tGoal (RecordMap Ident Type -> Type
TRec RecordMap Ident Type
tys)
ConstraintSource -> [Type] -> InferM ()
newGoals ConstraintSource
CtExactType [Type]
ps
Type
_ -> Error -> InferM ()
recordError (TypeSource -> Type -> Type -> Error
TypeMismatch TypeSource
src Type
ty (RecordMap Ident Type -> Type
TRec RecordMap Ident Type
tys))
RecordMap Ident (a, Type) -> InferM (RecordMap Ident (a, Type))
forall (m :: * -> *) a. Monad m => a -> m a
return RecordMap Ident (a, Type)
res
expectFin :: Int -> TypeWithSource -> InferM ()
expectFin :: Int -> TypeWithSource -> InferM ()
expectFin Int
n tGoal :: TypeWithSource
tGoal@(WithSource Type
ty TypeSource
src) =
case Type
ty of
TUser Name
_ [Type]
_ Type
ty' ->
Int -> TypeWithSource -> InferM ()
expectFin Int
n (Type -> TypeSource -> TypeWithSource
WithSource Type
ty' TypeSource
src)
TCon (TC (TCNum Integer
n')) [] | Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n' ->
() -> InferM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Type
_ -> ConstraintSource -> [Type] -> InferM ()
newGoals ConstraintSource
CtExactType ([Type] -> InferM ()) -> InferM [Type] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeWithSource -> Type -> InferM [Type]
unify TypeWithSource
tGoal (Int -> Type
forall a. Integral a => a -> Type
tNum Int
n)
expectFun :: Maybe Name -> Int -> TypeWithSource -> InferM ([Type],Type)
expectFun :: Maybe Name -> Int -> TypeWithSource -> InferM ([Type], Type)
expectFun Maybe Name
mbN Int
n (WithSource Type
ty0 TypeSource
src) = [Type] -> Int -> Type -> InferM ([Type], Type)
go [] Int
n Type
ty0
where
go :: [Type] -> Int -> Type -> InferM ([Type], Type)
go [Type]
tys Int
arity Type
ty
| Int
arity Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 =
case Type
ty of
TUser Name
_ [Type]
_ Type
ty' ->
[Type] -> Int -> Type -> InferM ([Type], Type)
go [Type]
tys Int
arity Type
ty'
TCon (TC TC
TCFun) [Type
a,Type
b] ->
[Type] -> Int -> Type -> InferM ([Type], Type)
go (Type
aType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
tys) (Int
arity Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Type
b
Type
_ ->
do [Type]
args <- Int -> InferM [Type]
genArgs Int
arity
Type
res <- TypeSource -> Kind -> InferM Type
newType TypeSource
TypeOfRes Kind
KType
case Type
ty of
TVar TVFree{} ->
do [Type]
ps <- TypeWithSource -> Type -> InferM [Type]
unify (Type -> TypeSource -> TypeWithSource
WithSource Type
ty TypeSource
src) ((Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
tFun Type
res [Type]
args)
ConstraintSource -> [Type] -> InferM ()
newGoals ConstraintSource
CtExactType [Type]
ps
Type
_ -> Error -> InferM ()
recordError (TypeSource -> Type -> Type -> Error
TypeMismatch TypeSource
src Type
ty ((Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
tFun Type
res [Type]
args))
([Type], Type) -> InferM ([Type], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
args, Type
res)
| Bool
otherwise =
([Type], Type) -> InferM ([Type], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
tys, Type
ty)
genArgs :: Int -> InferM [Type]
genArgs Int
arity = [Int] -> (Int -> InferM Type) -> InferM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ Int
1 .. Int
arity ] ((Int -> InferM Type) -> InferM [Type])
-> (Int -> InferM Type) -> InferM [Type]
forall a b. (a -> b) -> a -> b
$
\ Int
ix -> TypeSource -> Kind -> InferM Type
newType (ArgDescr -> TypeSource
TypeOfArg (Maybe Name -> Maybe Int -> ArgDescr
ArgDescr Maybe Name
mbN (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
ix))) Kind
KType
checkHasType :: Type -> TypeWithSource -> InferM ()
checkHasType :: Type -> TypeWithSource -> InferM ()
checkHasType Type
inferredType TypeWithSource
tGoal =
do [Type]
ps <- TypeWithSource -> Type -> InferM [Type]
unify TypeWithSource
tGoal Type
inferredType
case [Type]
ps of
[] -> () -> InferM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
[Type]
_ -> ConstraintSource -> [Type] -> InferM ()
newGoals ConstraintSource
CtExactType [Type]
ps
checkFun ::
P.FunDesc Name -> [P.Pattern Name] ->
P.Expr Name -> TypeWithSource -> InferM Expr
checkFun :: FunDesc Name
-> [Pattern Name] -> Expr Name -> TypeWithSource -> InferM Expr
checkFun FunDesc Name
_ [] Expr Name
e TypeWithSource
tGoal = Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
tGoal
checkFun (P.FunDesc Maybe Name
fun Int
offset) [Pattern Name]
ps Expr Name
e TypeWithSource
tGoal =
InferM Expr -> InferM Expr
forall a. InferM a -> InferM a
inNewScope
do let descs :: [TypeSource]
descs = [ ArgDescr -> TypeSource
TypeOfArg (Maybe Name -> Maybe Int -> ArgDescr
ArgDescr Maybe Name
fun (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n)) | Int
n <- [ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
offset .. ] ]
([Type]
tys,Type
tRes) <- Maybe Name -> Int -> TypeWithSource -> InferM ([Type], Type)
expectFun Maybe Name
fun ([Pattern Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern Name]
ps) TypeWithSource
tGoal
[Located Name]
largs <- [InferM (Located Name)] -> InferM [Located Name]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((Pattern Name -> TypeWithSource -> InferM (Located Name))
-> [Pattern Name] -> [TypeWithSource] -> [InferM (Located Name)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Pattern Name -> TypeWithSource -> InferM (Located Name)
checkP [Pattern Name]
ps ((Type -> TypeSource -> TypeWithSource)
-> [Type] -> [TypeSource] -> [TypeWithSource]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type -> TypeSource -> TypeWithSource
WithSource [Type]
tys [TypeSource]
descs))
let ds :: Map Name (Located Type)
ds = [(Name, Located Type)] -> Map Name (Located Type)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Located Name -> Name
forall a. Located a -> a
thing Located Name
x, Located Name
x { thing :: Type
thing = Type
t }) | (Located Name
x,Type
t) <- [Located Name] -> [Type] -> [(Located Name, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Located Name]
largs [Type]
tys ]
Expr
e1 <- Map Name (Located Type) -> InferM Expr -> InferM Expr
forall a. Map Name (Located Type) -> InferM a -> InferM a
withMonoTypes Map Name (Located Type)
ds (Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Type -> TypeSource -> TypeWithSource
WithSource Type
tRes TypeSource
TypeOfRes))
let args :: [(Name, Type)]
args = [ (Located Name -> Name
forall a. Located a -> a
thing Located Name
x, Type
t) | (Located Name
x,Type
t) <- [Located Name] -> [Type] -> [(Located Name, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Located Name]
largs [Type]
tys ]
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, Type) -> Expr -> Expr) -> Expr -> [(Name, Type)] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Name
x,Type
t) Expr
b -> Name -> Type -> Expr -> Expr
EAbs Name
x Type
t Expr
b) Expr
e1 [(Name, Type)]
args)
smallest :: [Type] -> InferM Type
smallest :: [Type] -> InferM Type
smallest [] = TypeSource -> Kind -> InferM Type
newType TypeSource
LenOfSeq Kind
KNum
smallest [Type
t] = Type -> InferM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
smallest [Type]
ts = do Type
a <- TypeSource -> Kind -> InferM Type
newType TypeSource
LenOfSeq Kind
KNum
ConstraintSource -> [Type] -> InferM ()
newGoals ConstraintSource
CtComprehension [ Type
a Type -> Type -> Type
=#= (Type -> Type -> Type) -> [Type] -> Type
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
tMin [Type]
ts ]
Type -> InferM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
a
checkP :: P.Pattern Name -> TypeWithSource -> InferM (Located Name)
checkP :: Pattern Name -> TypeWithSource -> InferM (Located Name)
checkP Pattern Name
p tGoal :: TypeWithSource
tGoal@(WithSource Type
_ TypeSource
src) =
do (Name
x, Located Type
t) <- Pattern Name -> InferM (Name, Located Type)
inferP Pattern Name
p
[Type]
ps <- TypeWithSource -> Type -> InferM [Type]
unify TypeWithSource
tGoal (Located Type -> Type
forall a. Located a -> a
thing Located Type
t)
let rng :: Range
rng = Range -> Maybe Range -> Range
forall a. a -> Maybe a -> a
fromMaybe Range
emptyRange (Pattern Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Pattern Name
p)
let mkErr :: Type -> InferM ()
mkErr = Error -> InferM ()
recordError (Error -> InferM ()) -> (Type -> Error) -> Type -> InferM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Goal] -> Error
UnsolvedGoals ([Goal] -> Error) -> (Type -> [Goal]) -> Type -> Error
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Goal -> [Goal] -> [Goal]
forall a. a -> [a] -> [a]
:[])
(Goal -> [Goal]) -> (Type -> Goal) -> Type -> [Goal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstraintSource -> Range -> Type -> Goal
Goal (TypeSource -> ConstraintSource
CtPattern TypeSource
src) Range
rng
(Type -> InferM ()) -> [Type] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> InferM ()
mkErr [Type]
ps
Located Name -> InferM (Located Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Range -> Name -> Located Name
forall a. Range -> a -> Located a
Located (Located Type -> Range
forall a. Located a -> Range
srcRange Located Type
t) Name
x)
inferP :: P.Pattern Name -> InferM (Name, Located Type)
inferP :: Pattern Name -> InferM (Name, Located Type)
inferP Pattern Name
pat =
case Pattern Name
pat of
P.PVar Located Name
x0 ->
do Type
a <- Range -> InferM Type -> InferM Type
forall a. Range -> InferM a -> InferM a
inRange (Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
x0) (TypeSource -> Kind -> InferM Type
newType (Name -> TypeSource
DefinitionOf (Located Name -> Name
forall a. Located a -> a
thing Located Name
x0)) Kind
KType)
(Name, Located Type) -> InferM (Name, Located Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Located Name -> Name
forall a. Located a -> a
thing Located Name
x0, Located Name
x0 { thing :: Type
thing = Type
a })
P.PTyped Pattern Name
p Type Name
t ->
do Type
tSig <- Type Name -> Kind -> InferM Type
checkTypeOfKind Type Name
t Kind
KType
Located Name
ln <- Pattern Name -> TypeWithSource -> InferM (Located Name)
checkP Pattern Name
p (Type -> TypeSource -> TypeWithSource
WithSource Type
tSig TypeSource
TypeFromUserAnnotation)
(Name, Located Type) -> InferM (Name, Located Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Located Name -> Name
forall a. Located a -> a
thing Located Name
ln, Located Name
ln { thing :: Type
thing = Type
tSig })
Pattern Name
_ -> String -> [String] -> InferM (Name, Located Type)
forall a. String -> [String] -> a
tcPanic String
"inferP" [ String
"Unexpected pattern:", Pattern Name -> String
forall a. Show a => a -> String
show Pattern Name
pat ]
inferMatch :: P.Match Name -> InferM (Match, Name, Located Type, Type)
inferMatch :: Match Name -> InferM (Match, Name, Located Type, Type)
inferMatch (P.Match Pattern Name
p Expr Name
e) =
do (Name
x,Located Type
t) <- Pattern Name -> InferM (Name, Located Type)
inferP Pattern Name
p
Type
n <- TypeSource -> Kind -> InferM Type
newType TypeSource
LenOfCompGen Kind
KNum
Expr
e' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Type -> TypeSource -> TypeWithSource
WithSource (Type -> Type -> Type
tSeq Type
n (Located Type -> Type
forall a. Located a -> a
thing Located Type
t)) TypeSource
GeneratorOfListComp)
(Match, Name, Located Type, Type)
-> InferM (Match, Name, Located Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type -> Type -> Expr -> Match
From Name
x Type
n (Located Type -> Type
forall a. Located a -> a
thing Located Type
t) Expr
e', Name
x, Located Type
t, Type
n)
inferMatch (P.MatchLet Bind Name
b)
| Bind Name -> Bool
forall name. Bind name -> Bool
P.bMono Bind Name
b =
do let rng :: Range
rng = Located Name -> Range
forall a. Located a -> Range
srcRange (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)
Type
a <- Range -> InferM Type -> InferM Type
forall a. Range -> InferM a -> InferM a
inRange Range
rng (TypeSource -> Kind -> InferM Type
newType (Name -> TypeSource
DefinitionOf (Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b))) Kind
KType)
Decl
b1 <- Bind Name -> Type -> InferM Decl
checkMonoB Bind Name
b Type
a
(Match, Name, Located Type, Type)
-> InferM (Match, Name, Located Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Match
Let Decl
b1, Decl -> Name
dName Decl
b1, Range -> Type -> Located Type
forall a. Range -> a -> Located a
Located (Located Name -> Range
forall a. Located a -> Range
srcRange (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)) Type
a, Int -> Type
forall a. Integral a => a -> Type
tNum (Int
1::Int))
| Bool
otherwise = String -> [String] -> InferM (Match, Name, Located Type, Type)
forall a. String -> [String] -> a
tcPanic String
"inferMatch"
[ String
"Unexpected polymorphic match let:", Bind Name -> String
forall a. Show a => a -> String
show Bind Name
b ]
inferCArm :: Int -> [P.Match Name] -> InferM
( [Match]
, Map Name (Located Type)
, Type
)
inferCArm :: Int
-> [Match Name] -> InferM ([Match], Map Name (Located Type), Type)
inferCArm Int
_ [] = String
-> [String] -> InferM ([Match], Map Name (Located Type), Type)
forall a. HasCallStack => String -> [String] -> a
panic String
"inferCArm" [ String
"Empty comprehension arm" ]
inferCArm Int
_ [Match Name
m] =
do (Match
m1, Name
x, Located Type
t, Type
n) <- Match Name -> InferM (Match, Name, Located Type, Type)
inferMatch Match Name
m
([Match], Map Name (Located Type), Type)
-> InferM ([Match], Map Name (Located Type), Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Match
m1], Name -> Located Type -> Map Name (Located Type)
forall k a. k -> a -> Map k a
Map.singleton Name
x Located Type
t, Type
n)
inferCArm Int
armNum (Match Name
m : [Match Name]
ms) =
do (Match
m1, Name
x, Located Type
t, Type
n) <- Match Name -> InferM (Match, Name, Located Type, Type)
inferMatch Match Name
m
([Match]
ms', Map Name (Located Type)
ds, Type
n') <- (Name, Located Type)
-> InferM ([Match], Map Name (Located Type), Type)
-> InferM ([Match], Map Name (Located Type), Type)
forall a. (Name, Located Type) -> InferM a -> InferM a
withMonoType (Name
x,Located Type
t) (Int
-> [Match Name] -> InferM ([Match], Map Name (Located Type), Type)
inferCArm Int
armNum [Match Name]
ms)
ConstraintSource -> [Type] -> InferM ()
newGoals ConstraintSource
CtComprehension [ Type -> Type
pFin Type
n' ]
([Match], Map Name (Located Type), Type)
-> InferM ([Match], Map Name (Located Type), Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Match
m1 Match -> [Match] -> [Match]
forall a. a -> [a] -> [a]
: [Match]
ms', (Located Type -> Located Type -> Located Type)
-> Name
-> Located Type
-> Map Name (Located Type)
-> Map Name (Located Type)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (\Located Type
_ Located Type
old -> Located Type
old) Name
x Located Type
t Map Name (Located Type)
ds, Type -> Type -> Type
tMul Type
n Type
n')
inferBinds :: Bool -> Bool -> [P.Bind Name] -> InferM [Decl]
inferBinds :: Bool -> Bool -> [Bind Name] -> InferM [Decl]
inferBinds Bool
isTopLevel Bool
isRec [Bind Name]
binds =
do
Bool
monoBinds <- InferM Bool
getMonoBinds
let ([Bind Name]
sigs,[Bind Name]
noSigs) = (Bind Name -> Bool) -> [Bind Name] -> ([Bind Name], [Bind Name])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Maybe (Schema Name) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Schema Name) -> Bool)
-> (Bind Name -> Maybe (Schema Name)) -> Bind Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bind Name -> Maybe (Schema Name)
forall name. Bind name -> Maybe (Schema name)
P.bSignature) [Bind Name]
binds
monos :: [Bind Name]
monos = [Bind Name]
sigs [Bind Name] -> [Bind Name] -> [Bind Name]
forall a. [a] -> [a] -> [a]
++ [ Bind Name
b { bMono :: Bool
P.bMono = Bool
True } | Bind Name
b <- [Bind Name]
noSigs ]
binds' :: [Bind Name]
binds' | (Bind Name -> Bool) -> [Bind Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Bind Name -> Bool
forall name. Bind name -> Bool
P.bMono [Bind Name]
binds = [Bind Name]
monos
| Bool
monoBinds Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
isTopLevel = [Bind Name]
monos
| Bool
otherwise = [Bind Name]
binds
check :: Map Name Expr -> InferM ([Decl], [Decl])
check Map Name Expr
exprMap =
do ([(Name, VarType)]
newEnv,[Either (InferM Decl) (InferM Decl)]
todos) <- [((Name, VarType), Either (InferM Decl) (InferM Decl))]
-> ([(Name, VarType)], [Either (InferM Decl) (InferM Decl)])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((Name, VarType), Either (InferM Decl) (InferM Decl))]
-> ([(Name, VarType)], [Either (InferM Decl) (InferM Decl)]))
-> InferM [((Name, VarType), Either (InferM Decl) (InferM Decl))]
-> InferM ([(Name, VarType)], [Either (InferM Decl) (InferM Decl)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Bind Name
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl)))
-> [Bind Name]
-> InferM [((Name, VarType), Either (InferM Decl) (InferM Decl))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Map Name Expr
-> Bind Name
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
guessType Map Name Expr
exprMap) [Bind Name]
binds'
let otherEnv :: [(Name, VarType)]
otherEnv = ((Name, VarType) -> Bool) -> [(Name, VarType)] -> [(Name, VarType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name, VarType) -> Bool
forall a. (a, VarType) -> Bool
isExt [(Name, VarType)]
newEnv
let ([InferM Decl]
sigsAndMonos,[InferM Decl]
noSigGen) = [Either (InferM Decl) (InferM Decl)]
-> ([InferM Decl], [InferM Decl])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either (InferM Decl) (InferM Decl)]
todos
let prepGen :: InferM ([Decl], [Goal])
prepGen = InferM [Decl] -> InferM ([Decl], [Goal])
forall a. InferM a -> InferM (a, [Goal])
collectGoals
(InferM [Decl] -> InferM ([Decl], [Goal]))
-> InferM [Decl] -> InferM ([Decl], [Goal])
forall a b. (a -> b) -> a -> b
$ do [Decl]
bs <- [InferM Decl] -> InferM [Decl]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [InferM Decl]
noSigGen
InferM ()
simplifyAllConstraints
[Decl] -> InferM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return [Decl]
bs
if Bool
isRec
then
do ([Decl]
bs1,[Goal]
cs) <- [(Name, VarType)]
-> InferM ([Decl], [Goal]) -> InferM ([Decl], [Goal])
forall a. [(Name, VarType)] -> InferM a -> InferM a
withVarTypes [(Name, VarType)]
newEnv InferM ([Decl], [Goal])
prepGen
[Decl]
genCs <- [(Name, VarType)] -> InferM [Decl] -> InferM [Decl]
forall a. [(Name, VarType)] -> InferM a -> InferM a
withVarTypes [(Name, VarType)]
otherEnv ([Decl] -> [Goal] -> InferM [Decl]
generalize [Decl]
bs1 [Goal]
cs)
let newEnv' :: [(Name, VarType)]
newEnv' = (Decl -> (Name, VarType)) -> [Decl] -> [(Name, VarType)]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> (Name, VarType)
toExt [Decl]
bs1 [(Name, VarType)] -> [(Name, VarType)] -> [(Name, VarType)]
forall a. [a] -> [a] -> [a]
++ [(Name, VarType)]
otherEnv
[Decl]
done <- [(Name, VarType)] -> InferM [Decl] -> InferM [Decl]
forall a. [(Name, VarType)] -> InferM a -> InferM a
withVarTypes [(Name, VarType)]
newEnv' ([InferM Decl] -> InferM [Decl]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [InferM Decl]
sigsAndMonos)
([Decl], [Decl]) -> InferM ([Decl], [Decl])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl]
done,[Decl]
genCs)
else
do [Decl]
done <- [InferM Decl] -> InferM [Decl]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [InferM Decl]
sigsAndMonos
([Decl]
bs1, [Goal]
cs) <- InferM ([Decl], [Goal])
prepGen
[Decl]
genCs <- [Decl] -> [Goal] -> InferM [Decl]
generalize [Decl]
bs1 [Goal]
cs
([Decl], [Decl]) -> InferM ([Decl], [Decl])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl]
done,[Decl]
genCs)
rec
let exprMap :: Map Name Expr
exprMap = [(Name, Expr)] -> Map Name Expr
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ((Decl -> (Name, Expr)) -> [Decl] -> [(Name, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> (Name, Expr)
monoUse [Decl]
genBs)
([Decl]
doneBs, [Decl]
genBs) <- Map Name Expr -> InferM ([Decl], [Decl])
check Map Name Expr
exprMap
InferM ()
simplifyAllConstraints
[Decl] -> InferM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl]
doneBs [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++ [Decl]
genBs)
where
toExt :: Decl -> (Name, VarType)
toExt Decl
d = (Decl -> Name
dName Decl
d, Schema -> VarType
ExtVar (Decl -> Schema
dSignature Decl
d))
isExt :: (a, VarType) -> Bool
isExt (a
_,VarType
y) = case VarType
y of
ExtVar Schema
_ -> Bool
True
VarType
_ -> Bool
False
monoUse :: Decl -> (Name, Expr)
monoUse Decl
d = (Name
x, Expr
withQs)
where
x :: Name
x = Decl -> Name
dName Decl
d
as :: [TParam]
as = Schema -> [TParam]
sVars (Decl -> Schema
dSignature Decl
d)
qs :: [Type]
qs = Schema -> [Type]
sProps (Decl -> Schema
dSignature Decl
d)
appT :: Expr -> TParam -> Expr
appT Expr
e TParam
a = Expr -> Type -> Expr
ETApp Expr
e (TVar -> Type
TVar (TParam -> TVar
tpVar TParam
a))
appP :: Expr -> p -> Expr
appP Expr
e p
_ = Expr -> Expr
EProofApp Expr
e
withTys :: Expr
withTys = (Expr -> TParam -> Expr) -> Expr -> [TParam] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Expr -> TParam -> Expr
appT (Name -> Expr
EVar Name
x) [TParam]
as
withQs :: Expr
withQs = (Expr -> Type -> Expr) -> Expr -> [Type] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Expr -> Type -> Expr
forall p. Expr -> p -> Expr
appP Expr
withTys [Type]
qs
guessType :: Map Name Expr -> P.Bind Name ->
InferM ( (Name, VarType)
, Either (InferM Decl)
(InferM Decl)
)
guessType :: Map Name Expr
-> Bind Name
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
guessType Map Name Expr
exprMap b :: Bind Name
b@(P.Bind { Bool
[Pattern Name]
[Pragma]
Maybe Text
Maybe Fixity
Maybe (Schema Name)
Located Name
Located (BindDef Name)
ExportType
bExport :: forall name. Bind name -> ExportType
bDoc :: forall name. Bind name -> Maybe Text
bPragmas :: forall name. Bind name -> [Pragma]
bFixity :: forall name. Bind name -> Maybe Fixity
bInfix :: forall name. Bind name -> Bool
bDef :: forall name. Bind name -> Located (BindDef name)
bParams :: forall name. Bind name -> [Pattern name]
bExport :: ExportType
bDoc :: Maybe Text
bMono :: Bool
bPragmas :: [Pragma]
bFixity :: Maybe Fixity
bInfix :: Bool
bSignature :: Maybe (Schema Name)
bDef :: Located (BindDef Name)
bParams :: [Pattern Name]
bName :: Located Name
bSignature :: forall name. Bind name -> Maybe (Schema name)
bName :: forall name. Bind name -> Located name
bMono :: forall name. Bind name -> Bool
.. }) =
case Maybe (Schema Name)
bSignature of
Just Schema Name
s ->
do (Schema, [Goal])
s1 <- AllowWildCards -> Schema Name -> InferM (Schema, [Goal])
checkSchema AllowWildCards
AllowWildCards Schema Name
s
((Name, VarType), Either (InferM Decl) (InferM Decl))
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
name, Schema -> VarType
ExtVar ((Schema, [Goal]) -> Schema
forall a b. (a, b) -> a
fst (Schema, [Goal])
s1)), InferM Decl -> Either (InferM Decl) (InferM Decl)
forall a b. a -> Either a b
Left (Bind Name -> (Schema, [Goal]) -> InferM Decl
checkSigB Bind Name
b (Schema, [Goal])
s1))
Maybe (Schema Name)
Nothing
| Bool
bMono ->
do Type
t <- TypeSource -> Kind -> InferM Type
newType (Name -> TypeSource
DefinitionOf Name
name) Kind
KType
let schema :: Schema
schema = [TParam] -> [Type] -> Type -> Schema
Forall [] [] Type
t
((Name, VarType), Either (InferM Decl) (InferM Decl))
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
name, Schema -> VarType
ExtVar Schema
schema), InferM Decl -> Either (InferM Decl) (InferM Decl)
forall a b. a -> Either a b
Left (Bind Name -> Type -> InferM Decl
checkMonoB Bind Name
b Type
t))
| Bool
otherwise ->
do Type
t <- TypeSource -> Kind -> InferM Type
newType (Name -> TypeSource
DefinitionOf Name
name) Kind
KType
let noWay :: a
noWay = String -> [String] -> a
forall a. String -> [String] -> a
tcPanic String
"guessType" [ String
"Missing expression for:" ,
Name -> String
forall a. Show a => a -> String
show Name
name ]
expr :: Expr
expr = Expr -> Name -> Map Name Expr -> Expr
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Expr
forall a. a
noWay Name
name Map Name Expr
exprMap
((Name, VarType), Either (InferM Decl) (InferM Decl))
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
name, Expr -> Type -> VarType
CurSCC Expr
expr Type
t), InferM Decl -> Either (InferM Decl) (InferM Decl)
forall a b. b -> Either a b
Right (Bind Name -> Type -> InferM Decl
checkMonoB Bind Name
b Type
t))
where
name :: Name
name = Located Name -> Name
forall a. Located a -> a
thing Located Name
bName
generalize :: [Decl] -> [Goal] -> InferM [Decl]
generalize :: [Decl] -> [Goal] -> InferM [Decl]
generalize [] [Goal]
gs0 =
do [Goal] -> InferM ()
addGoals [Goal]
gs0
[Decl] -> InferM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return []
generalize [Decl]
bs0 [Goal]
gs0 =
do
[Goal]
gs <- [Goal] -> InferM [Goal]
applySubstGoals [Goal]
gs0
[Decl]
bs <- [Decl] -> (Decl -> InferM Decl) -> InferM [Decl]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Decl]
bs0 ((Decl -> InferM Decl) -> InferM [Decl])
-> (Decl -> InferM Decl) -> InferM [Decl]
forall a b. (a -> b) -> a -> b
$ \Decl
b -> do Schema
s <- Schema -> InferM Schema
forall t. TVars t => t -> InferM t
applySubst (Decl -> Schema
dSignature Decl
b)
Decl -> InferM Decl
forall (m :: * -> *) a. Monad m => a -> m a
return Decl
b { dSignature :: Schema
dSignature = Schema
s }
let goalFVS :: Goal -> Set TVar
goalFVS Goal
g = (TVar -> Bool) -> Set TVar -> Set TVar
forall a. (a -> Bool) -> Set a -> Set a
Set.filter TVar -> Bool
isFreeTV (Set TVar -> Set TVar) -> Set TVar -> Set TVar
forall a b. (a -> b) -> a -> b
$ Type -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (Type -> Set TVar) -> Type -> Set TVar
forall a b. (a -> b) -> a -> b
$ Goal -> Type
goal Goal
g
inGoals :: Set TVar
inGoals = [Set TVar] -> Set TVar
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set TVar] -> Set TVar) -> [Set TVar] -> Set TVar
forall a b. (a -> b) -> a -> b
$ (Goal -> Set TVar) -> [Goal] -> [Set TVar]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Set TVar
goalFVS [Goal]
gs
inSigs :: Set TVar
inSigs = (TVar -> Bool) -> Set TVar -> Set TVar
forall a. (a -> Bool) -> Set a -> Set a
Set.filter TVar -> Bool
isFreeTV (Set TVar -> Set TVar) -> Set TVar -> Set TVar
forall a b. (a -> b) -> a -> b
$ [Schema] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs ([Schema] -> Set TVar) -> [Schema] -> Set TVar
forall a b. (a -> b) -> a -> b
$ (Decl -> Schema) -> [Decl] -> [Schema]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> Schema
dSignature [Decl]
bs
candidates :: Set TVar
candidates = (Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set TVar
inGoals Set TVar
inSigs)
Set TVar
asmpVs <- InferM (Set TVar)
varsWithAsmps
let gen0 :: Set TVar
gen0 = Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set TVar
candidates Set TVar
asmpVs
stays :: Goal -> Bool
stays Goal
g = (TVar -> Bool) -> [TVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
gen0) ([TVar] -> Bool) -> [TVar] -> Bool
forall a b. (a -> b) -> a -> b
$ Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (Set TVar -> [TVar]) -> Set TVar -> [TVar]
forall a b. (a -> b) -> a -> b
$ Goal -> Set TVar
goalFVS Goal
g
([Goal]
here0,[Goal]
later) = (Goal -> Bool) -> [Goal] -> ([Goal], [Goal])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Goal -> Bool
stays [Goal]
gs
[Goal] -> InferM ()
addGoals [Goal]
later
let maybeAmbig :: [TVar]
maybeAmbig = Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set TVar
gen0 Set TVar
inSigs)
let ([TVar]
as0,[Goal]
here1,Subst
defSu,[Warning]
ws,[Error]
errs) = [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning], [Error])
defaultAndSimplify [TVar]
maybeAmbig [Goal]
here0
Subst -> InferM ()
extendSubst Subst
defSu
(Warning -> InferM ()) -> [Warning] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Warning -> InferM ()
recordWarning [Warning]
ws
(Error -> InferM ()) -> [Error] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Error -> InferM ()
recordError [Error]
errs
let here :: [Type]
here = (Goal -> Type) -> [Goal] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Type
goal [Goal]
here1
let as :: [TVar]
as = (TVar -> TVar -> Ordering) -> [TVar] -> [TVar]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy TVar -> TVar -> Ordering
forall t t. (HasKind t, HasKind t) => t -> t -> Ordering
numFst
([TVar] -> [TVar]) -> [TVar] -> [TVar]
forall a b. (a -> b) -> a -> b
$ [TVar]
as0 [TVar] -> [TVar] -> [TVar]
forall a. [a] -> [a] -> [a]
++ Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set TVar
inSigs Set TVar
asmpVs)
asPs :: [TParam]
asPs = [ TParam :: Int -> Kind -> TPFlavor -> TVarInfo -> TParam
TParam { tpUnique :: Int
tpUnique = Int
x
, tpKind :: Kind
tpKind = Kind
k
, tpFlav :: TPFlavor
tpFlav = TPFlavor
TPUnifyVar
, tpInfo :: TVarInfo
tpInfo = TVarInfo
i
}
| TVFree Int
x Kind
k Set TParam
_ TVarInfo
i <- [TVar]
as
]
Subst
totSu <- InferM Subst
getSubst
let
su :: Subst
su = [(TVar, Type)] -> Subst
listSubst ([TVar] -> [Type] -> [(TVar, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TVar]
as ((TParam -> Type) -> [TParam] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (TVar -> Type
TVar (TVar -> Type) -> (TParam -> TVar) -> TParam -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
tpVar) [TParam]
asPs)) Subst -> Subst -> Subst
@@ Subst
totSu
qs :: [Type]
qs = (Type -> [Type]) -> [Type] -> [Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Type -> [Type]
pSplitAnd (Type -> [Type]) -> (Type -> Type) -> Type -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su) [Type]
here
genE :: Expr -> Expr
genE Expr
e = (TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs ((Type -> Expr -> Expr) -> Expr -> [Type] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Expr -> Expr
EProofAbs (Subst -> Expr -> Expr
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e) [Type]
qs) [TParam]
asPs
genB :: Decl -> Decl
genB Decl
d = Decl
d { dDefinition :: DeclDef
dDefinition = case Decl -> DeclDef
dDefinition Decl
d of
DExpr Expr
e -> Expr -> DeclDef
DExpr (Expr -> Expr
genE Expr
e)
DeclDef
DPrim -> DeclDef
DPrim
, dSignature :: Schema
dSignature = [TParam] -> [Type] -> Type -> Schema
Forall [TParam]
asPs [Type]
qs
(Type -> Schema) -> Type -> Schema
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Schema -> Type
sType (Schema -> Type) -> Schema -> Type
forall a b. (a -> b) -> a -> b
$ Decl -> Schema
dSignature Decl
d
}
[Decl] -> InferM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Decl -> Decl) -> [Decl] -> [Decl]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> Decl
genB [Decl]
bs)
where
numFst :: t -> t -> Ordering
numFst t
x t
y = case (t -> Kind
forall t. HasKind t => t -> Kind
kindOf t
x, t -> Kind
forall t. HasKind t => t -> Kind
kindOf t
y) of
(Kind
KNum, Kind
KNum) -> Ordering
EQ
(Kind
KNum, Kind
_) -> Ordering
LT
(Kind
_,Kind
KNum) -> Ordering
GT
(Kind, Kind)
_ -> Ordering
EQ
checkMonoB :: P.Bind Name -> Type -> InferM Decl
checkMonoB :: Bind Name -> Type -> InferM Decl
checkMonoB Bind Name
b Type
t =
Maybe Range -> InferM Decl -> InferM Decl
forall a. Maybe Range -> InferM a -> InferM a
inRangeMb (Bind Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Bind Name
b) (InferM Decl -> InferM Decl) -> InferM Decl -> InferM Decl
forall a b. (a -> b) -> a -> b
$
case Located (BindDef Name) -> BindDef Name
forall a. Located a -> a
thing (Bind Name -> Located (BindDef Name)
forall name. Bind name -> Located (BindDef name)
P.bDef Bind Name
b) of
BindDef Name
P.DPrim -> String -> [String] -> InferM Decl
forall a. HasCallStack => String -> [String] -> a
panic String
"checkMonoB" [String
"Primitive with no signature?"]
P.DExpr Expr Name
e ->
do let nm :: Name
nm = Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)
let tGoal :: TypeWithSource
tGoal = Type -> TypeSource -> TypeWithSource
WithSource Type
t (Name -> TypeSource
DefinitionOf Name
nm)
Expr
e1 <- FunDesc Name
-> [Pattern Name] -> Expr Name -> TypeWithSource -> InferM Expr
checkFun (Maybe Name -> Int -> FunDesc Name
forall n. Maybe n -> Int -> FunDesc n
P.FunDesc (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
nm) Int
0) (Bind Name -> [Pattern Name]
forall name. Bind name -> [Pattern name]
P.bParams Bind Name
b) Expr Name
e TypeWithSource
tGoal
let f :: Name
f = Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)
Decl -> InferM Decl
forall (m :: * -> *) a. Monad m => a -> m a
return Decl :: Name
-> Schema
-> DeclDef
-> [Pragma]
-> Bool
-> Maybe Fixity
-> Maybe Text
-> Decl
Decl { dName :: Name
dName = Name
f
, dSignature :: Schema
dSignature = [TParam] -> [Type] -> Type -> Schema
Forall [] [] Type
t
, dDefinition :: DeclDef
dDefinition = Expr -> DeclDef
DExpr Expr
e1
, dPragmas :: [Pragma]
dPragmas = Bind Name -> [Pragma]
forall name. Bind name -> [Pragma]
P.bPragmas Bind Name
b
, dInfix :: Bool
dInfix = Bind Name -> Bool
forall name. Bind name -> Bool
P.bInfix Bind Name
b
, dFixity :: Maybe Fixity
dFixity = Bind Name -> Maybe Fixity
forall name. Bind name -> Maybe Fixity
P.bFixity Bind Name
b
, dDoc :: Maybe Text
dDoc = Bind Name -> Maybe Text
forall name. Bind name -> Maybe Text
P.bDoc Bind Name
b
}
checkSigB :: P.Bind Name -> (Schema,[Goal]) -> InferM Decl
checkSigB :: Bind Name -> (Schema, [Goal]) -> InferM Decl
checkSigB Bind Name
b (Forall [TParam]
as [Type]
asmps0 Type
t0, [Goal]
validSchema) = case Located (BindDef Name) -> BindDef Name
forall a. Located a -> a
thing (Bind Name -> Located (BindDef Name)
forall name. Bind name -> Located (BindDef name)
P.bDef Bind Name
b) of
BindDef Name
P.DPrim ->
do Decl -> InferM Decl
forall (m :: * -> *) a. Monad m => a -> m a
return Decl :: Name
-> Schema
-> DeclDef
-> [Pragma]
-> Bool
-> Maybe Fixity
-> Maybe Text
-> Decl
Decl { dName :: Name
dName = Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)
, dSignature :: Schema
dSignature = [TParam] -> [Type] -> Type -> Schema
Forall [TParam]
as [Type]
asmps0 Type
t0
, dDefinition :: DeclDef
dDefinition = DeclDef
DPrim
, dPragmas :: [Pragma]
dPragmas = Bind Name -> [Pragma]
forall name. Bind name -> [Pragma]
P.bPragmas Bind Name
b
, dInfix :: Bool
dInfix = Bind Name -> Bool
forall name. Bind name -> Bool
P.bInfix Bind Name
b
, dFixity :: Maybe Fixity
dFixity = Bind Name -> Maybe Fixity
forall name. Bind name -> Maybe Fixity
P.bFixity Bind Name
b
, dDoc :: Maybe Text
dDoc = Bind Name -> Maybe Text
forall name. Bind name -> Maybe Text
P.bDoc Bind Name
b
}
P.DExpr Expr Name
e0 ->
Maybe Range -> InferM Decl -> InferM Decl
forall a. Maybe Range -> InferM a -> InferM a
inRangeMb (Bind Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Bind Name
b) (InferM Decl -> InferM Decl) -> InferM Decl -> InferM Decl
forall a b. (a -> b) -> a -> b
$
[TParam] -> InferM Decl -> InferM Decl
forall a. [TParam] -> InferM a -> InferM a
withTParams [TParam]
as (InferM Decl -> InferM Decl) -> InferM Decl -> InferM Decl
forall a b. (a -> b) -> a -> b
$
do (Expr
e1,[Goal]
cs0) <- InferM Expr -> InferM (Expr, [Goal])
forall a. InferM a -> InferM (a, [Goal])
collectGoals (InferM Expr -> InferM (Expr, [Goal]))
-> InferM Expr -> InferM (Expr, [Goal])
forall a b. (a -> b) -> a -> b
$
do let nm :: Name
nm = Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)
tGoal :: TypeWithSource
tGoal = Type -> TypeSource -> TypeWithSource
WithSource Type
t0 (Name -> TypeSource
DefinitionOf Name
nm)
Expr
e1 <- FunDesc Name
-> [Pattern Name] -> Expr Name -> TypeWithSource -> InferM Expr
checkFun (Maybe Name -> Int -> FunDesc Name
forall n. Maybe n -> Int -> FunDesc n
P.FunDesc (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
nm) Int
0) (Bind Name -> [Pattern Name]
forall name. Bind name -> [Pattern name]
P.bParams Bind Name
b) Expr Name
e0 TypeWithSource
tGoal
[Goal] -> InferM ()
addGoals [Goal]
validSchema
() <- InferM ()
simplifyAllConstraints
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e1
[Type]
asmps1 <- [Type] -> InferM [Type]
applySubstPreds [Type]
asmps0
[Goal]
cs <- [Goal] -> InferM [Goal]
applySubstGoals [Goal]
cs0
let findKeep :: Set a -> [a] -> [(a, Set a)] -> ([a], [a])
findKeep Set a
vs [a]
keep [(a, Set a)]
todo =
let stays :: (a, Set a) -> Bool
stays (a
_,Set a
cvs) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set a -> Bool
forall a. Set a -> Bool
Set.null (Set a -> Bool) -> Set a -> Bool
forall a b. (a -> b) -> a -> b
$ Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set a
vs Set a
cvs
([(a, Set a)]
yes,[(a, Set a)]
perhaps) = ((a, Set a) -> Bool)
-> [(a, Set a)] -> ([(a, Set a)], [(a, Set a)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (a, Set a) -> Bool
forall a. (a, Set a) -> Bool
stays [(a, Set a)]
todo
([a]
stayPs,[Set a]
newVars) = [(a, Set a)] -> ([a], [Set a])
forall a b. [(a, b)] -> ([a], [b])
unzip [(a, Set a)]
yes
in case [a]
stayPs of
[] -> ([a]
keep,((a, Set a) -> a) -> [(a, Set a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, Set a) -> a
forall a b. (a, b) -> a
fst [(a, Set a)]
todo)
[a]
_ -> Set a -> [a] -> [(a, Set a)] -> ([a], [a])
findKeep ([Set a] -> Set a
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (Set a
vsSet a -> [Set a] -> [Set a]
forall a. a -> [a] -> [a]
:[Set a]
newVars)) ([a]
stayPs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
keep) [(a, Set a)]
perhaps
let
stickyVars :: Set TVar
stickyVars = [TVar] -> Set TVar
forall a. Ord a => [a] -> Set a
Set.fromList ((TParam -> TVar) -> [TParam] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar [TParam]
as) Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` [Type] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs [Type]
asmps1
([Goal]
stay,[Goal]
leave) = Set TVar -> [Goal] -> [(Goal, Set TVar)] -> ([Goal], [Goal])
forall a a. Ord a => Set a -> [a] -> [(a, Set a)] -> ([a], [a])
findKeep Set TVar
stickyVars []
[ (Goal
c, Goal -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Goal
c) | Goal
c <- [Goal]
cs ]
[Goal] -> InferM ()
addGoals [Goal]
leave
Subst
su <- Maybe Name -> [TParam] -> [Type] -> [Goal] -> InferM Subst
proveImplication (Name -> Maybe Name
forall a. a -> Maybe a
Just (Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b))) [TParam]
as [Type]
asmps1 [Goal]
stay
Subst -> InferM ()
extendSubst Subst
su
let asmps :: [Type]
asmps = (Type -> [Type]) -> [Type] -> [Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
pSplitAnd (Subst -> [Type] -> [Type]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Type]
asmps1)
Type
t <- Type -> InferM Type
forall t. TVars t => t -> InferM t
applySubst Type
t0
Expr
e2 <- Expr -> InferM Expr
forall t. TVars t => t -> InferM t
applySubst Expr
e1
Decl -> InferM Decl
forall (m :: * -> *) a. Monad m => a -> m a
return Decl :: Name
-> Schema
-> DeclDef
-> [Pragma]
-> Bool
-> Maybe Fixity
-> Maybe Text
-> Decl
Decl
{ dName :: Name
dName = Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)
, dSignature :: Schema
dSignature = [TParam] -> [Type] -> Type -> Schema
Forall [TParam]
as [Type]
asmps Type
t
, dDefinition :: DeclDef
dDefinition = Expr -> DeclDef
DExpr ((TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs ((Type -> Expr -> Expr) -> Expr -> [Type] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Expr -> Expr
EProofAbs Expr
e2 [Type]
asmps) [TParam]
as)
, dPragmas :: [Pragma]
dPragmas = Bind Name -> [Pragma]
forall name. Bind name -> [Pragma]
P.bPragmas Bind Name
b
, dInfix :: Bool
dInfix = Bind Name -> Bool
forall name. Bind name -> Bool
P.bInfix Bind Name
b
, dFixity :: Maybe Fixity
dFixity = Bind Name -> Maybe Fixity
forall name. Bind name -> Maybe Fixity
P.bFixity Bind Name
b
, dDoc :: Maybe Text
dDoc = Bind Name -> Maybe Text
forall name. Bind name -> Maybe Text
P.bDoc Bind Name
b
}
checkLocalDecls :: [P.Decl Name] -> InferM a -> InferM (a,[DeclGroup])
checkLocalDecls :: [Decl Name] -> InferM a -> InferM (a, [DeclGroup])
checkLocalDecls [Decl Name]
ds0 InferM a
k =
do InferM ()
newLocalScope
[Decl Name] -> (Decl Name -> InferM ()) -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Decl Name]
ds0 \Decl Name
d -> Bool -> Decl Name -> Maybe Text -> InferM ()
checkDecl Bool
False Decl Name
d Maybe Text
forall a. Maybe a
Nothing
a
a <- InferM a
k
([DeclGroup]
ds,Map Name TySyn
_tySyns) <- InferM ([DeclGroup], Map Name TySyn)
endLocalScope
(a, [DeclGroup]) -> InferM (a, [DeclGroup])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a,[DeclGroup]
ds)
checkTopDecls :: [P.TopDecl Name] -> InferM ()
checkTopDecls :: [TopDecl Name] -> InferM ()
checkTopDecls = (TopDecl Name -> InferM ()) -> [TopDecl Name] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TopDecl Name -> InferM ()
checkTopDecl
where
checkTopDecl :: TopDecl Name -> InferM ()
checkTopDecl TopDecl Name
decl =
case TopDecl Name
decl of
P.Decl TopLevel (Decl Name)
tl -> Bool -> Decl Name -> Maybe Text -> InferM ()
checkDecl Bool
True (TopLevel (Decl Name) -> Decl Name
forall a. TopLevel a -> a
P.tlValue TopLevel (Decl Name)
tl) (Located Text -> Text
forall a. Located a -> a
thing (Located Text -> Text) -> Maybe (Located Text) -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevel (Decl Name) -> Maybe (Located Text)
forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (Decl Name)
tl)
P.TDNewtype TopLevel (Newtype Name)
tl ->
do Newtype
t <- Newtype Name -> Maybe Text -> InferM Newtype
checkNewtype (TopLevel (Newtype Name) -> Newtype Name
forall a. TopLevel a -> a
P.tlValue TopLevel (Newtype Name)
tl) (Located Text -> Text
forall a. Located a -> a
thing (Located Text -> Text) -> Maybe (Located Text) -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevel (Newtype Name) -> Maybe (Located Text)
forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (Newtype Name)
tl)
Newtype -> InferM ()
addNewtype Newtype
t
P.DPrimType TopLevel (PrimType Name)
tl ->
do AbstractType
t <- PrimType Name -> Maybe Text -> InferM AbstractType
checkPrimType (TopLevel (PrimType Name) -> PrimType Name
forall a. TopLevel a -> a
P.tlValue TopLevel (PrimType Name)
tl) (Located Text -> Text
forall a. Located a -> a
thing (Located Text -> Text) -> Maybe (Located Text) -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevel (PrimType Name) -> Maybe (Located Text)
forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (PrimType Name)
tl)
AbstractType -> InferM ()
addPrimType AbstractType
t
P.DParameterType ParameterType Name
ty ->
do ModTParam
t <- ParameterType Name -> Maybe Text -> InferM ModTParam
checkParameterType ParameterType Name
ty (ParameterType Name -> Maybe Text
forall name. ParameterType name -> Maybe Text
P.ptDoc ParameterType Name
ty)
ModTParam -> InferM ()
addParamType ModTParam
t
P.DParameterConstraint [Located (Prop Name)]
cs ->
do [Located Type]
cs1 <- [Located (Prop Name)] -> InferM [Located Type]
checkParameterConstraints [Located (Prop Name)]
cs
[Located Type] -> InferM ()
addParameterConstraints [Located Type]
cs1
P.DParameterFun ParameterFun Name
pf ->
do ModVParam
x <- ParameterFun Name -> InferM ModVParam
checkParameterFun ParameterFun Name
pf
ModVParam -> InferM ()
addParamFun ModVParam
x
P.DModule TopLevel (NestedModule Name)
tl ->
do let P.NestedModule ModuleG Name Name
m = TopLevel (NestedModule Name) -> NestedModule Name
forall a. TopLevel a -> a
P.tlValue TopLevel (NestedModule Name)
tl
Name -> [Import] -> ExportSpec Name -> InferM ()
newSubmoduleScope (Located Name -> Name
forall a. Located a -> a
thing (ModuleG Name Name -> Located Name
forall mname name. ModuleG mname name -> Located mname
P.mName ModuleG Name Name
m)) ((Located Import -> Import) -> [Located Import] -> [Import]
forall a b. (a -> b) -> [a] -> [b]
map Located Import -> Import
forall a. Located a -> a
thing (ModuleG Name Name -> [Located Import]
forall mname name. ModuleG mname name -> [Located Import]
P.mImports ModuleG Name Name
m))
(ModuleG Name Name -> ExportSpec Name
forall name mname.
Ord name =>
ModuleG mname name -> ExportSpec name
P.modExports ModuleG Name Name
m)
[TopDecl Name] -> InferM ()
checkTopDecls (ModuleG Name Name -> [TopDecl Name]
forall mname name. ModuleG mname name -> [TopDecl name]
P.mDecls ModuleG Name Name
m)
InferM ()
endSubmodule
P.DImport {} -> () -> InferM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
P.Include {} -> String -> [String] -> InferM ()
forall a. HasCallStack => String -> [String] -> a
panic String
"checkTopDecl" [ String
"Unexpected `inlude`" ]
checkDecl :: Bool -> P.Decl Name -> Maybe Text -> InferM ()
checkDecl :: Bool -> Decl Name -> Maybe Text -> InferM ()
checkDecl Bool
isTopLevel Decl Name
d Maybe Text
mbDoc =
case Decl Name
d of
P.DBind Bind Name
c ->
do ~[Decl
b] <- Bool -> Bool -> [Bind Name] -> InferM [Decl]
inferBinds Bool
isTopLevel Bool
False [Bind Name
c]
DeclGroup -> InferM ()
addDecls (Decl -> DeclGroup
NonRecursive Decl
b)
P.DRec [Bind Name]
bs ->
do [Decl]
bs1 <- Bool -> Bool -> [Bind Name] -> InferM [Decl]
inferBinds Bool
isTopLevel Bool
True [Bind Name]
bs
DeclGroup -> InferM ()
addDecls ([Decl] -> DeclGroup
Recursive [Decl]
bs1)
P.DType TySyn Name
t ->
do TySyn
t1 <- TySyn Name -> Maybe Text -> InferM TySyn
checkTySyn TySyn Name
t Maybe Text
mbDoc
TySyn -> InferM ()
addTySyn TySyn
t1
P.DProp PropSyn Name
t ->
do TySyn
t1 <- PropSyn Name -> Maybe Text -> InferM TySyn
checkPropSyn PropSyn Name
t Maybe Text
mbDoc
TySyn -> InferM ()
addTySyn TySyn
t1
P.DLocated Decl Name
d' Range
r -> Range -> InferM () -> InferM ()
forall a. Range -> InferM a -> InferM a
inRange Range
r (Bool -> Decl Name -> Maybe Text -> InferM ()
checkDecl Bool
isTopLevel Decl Name
d' Maybe Text
mbDoc)
P.DSignature {} -> String -> InferM ()
forall a. String -> a
bad String
"DSignature"
P.DFixity {} -> String -> InferM ()
forall a. String -> a
bad String
"DFixity"
P.DPragma {} -> String -> InferM ()
forall a. String -> a
bad String
"DPragma"
P.DPatBind {} -> String -> InferM ()
forall a. String -> a
bad String
"DPatBind"
where
bad :: String -> a
bad String
x = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"checkDecl" [String
x]
checkParameterFun :: P.ParameterFun Name -> InferM ModVParam
checkParameterFun :: ParameterFun Name -> InferM ModVParam
checkParameterFun ParameterFun Name
x =
do (Schema
s,[Goal]
gs) <- AllowWildCards -> Schema Name -> InferM (Schema, [Goal])
checkSchema AllowWildCards
NoWildCards (ParameterFun Name -> Schema Name
forall name. ParameterFun name -> Schema name
P.pfSchema ParameterFun Name
x)
Subst
su <- Maybe Name -> [TParam] -> [Type] -> [Goal] -> InferM Subst
proveImplication (Name -> Maybe Name
forall a. a -> Maybe a
Just (Located Name -> Name
forall a. Located a -> a
thing (ParameterFun Name -> Located Name
forall name. ParameterFun name -> Located name
P.pfName ParameterFun Name
x)))
(Schema -> [TParam]
sVars Schema
s) (Schema -> [Type]
sProps Schema
s) [Goal]
gs
Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Subst -> Bool
isEmptySubst Subst
su) (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$
String -> [String] -> InferM ()
forall a. HasCallStack => String -> [String] -> a
panic String
"checkParameterFun" [String
"Subst not empty??"]
let n :: Name
n = Located Name -> Name
forall a. Located a -> a
thing (ParameterFun Name -> Located Name
forall name. ParameterFun name -> Located name
P.pfName ParameterFun Name
x)
ModVParam -> InferM ModVParam
forall (m :: * -> *) a. Monad m => a -> m a
return ModVParam :: Name -> Schema -> Maybe Text -> Maybe Fixity -> ModVParam
ModVParam { mvpName :: Name
mvpName = Name
n
, mvpType :: Schema
mvpType = Schema
s
, mvpDoc :: Maybe Text
mvpDoc = ParameterFun Name -> Maybe Text
forall name. ParameterFun name -> Maybe Text
P.pfDoc ParameterFun Name
x
, mvpFixity :: Maybe Fixity
mvpFixity = ParameterFun Name -> Maybe Fixity
forall name. ParameterFun name -> Maybe Fixity
P.pfFixity ParameterFun Name
x
}
tcPanic :: String -> [String] -> a
tcPanic :: String -> [String] -> a
tcPanic String
l [String]
msg = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic (String
"[TypeCheck] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
l) [String]
msg