{-# Language OverloadedStrings #-}
module Cryptol.TypeCheck.Sanity
( tcExpr
, tcDecls
, tcModule
, ProofObligation
, onlyNonTrivial
, Error(..)
, AreSame(..)
, same
) where
import Cryptol.Parser.Position(thing,Range,emptyRange)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst (apSubst, singleTParamSubst)
import Cryptol.TypeCheck.Monad(InferInput(..))
import Cryptol.ModuleSystem.Name(nameLoc)
import Cryptol.Utils.Ident
import Cryptol.Utils.RecordMap
import Cryptol.Utils.PP
import Data.List (sort)
import qualified Data.Set as Set
import MonadLib
import qualified Control.Applicative as A
import Data.Map ( Map )
import qualified Data.Map as Map
tcExpr :: InferInput -> Expr -> Either (Range, Error) (Schema, [ ProofObligation ])
tcExpr :: InferInput -> Expr -> Either (Range, Error) (Schema, [Schema])
tcExpr InferInput
env Expr
e = InferInput
-> TcM Schema -> Either (Range, Error) (Schema, [Schema])
forall a.
InferInput -> TcM a -> Either (Range, Error) (a, [Schema])
runTcM InferInput
env (Expr -> TcM Schema
exprSchema Expr
e)
tcDecls :: InferInput -> [DeclGroup] -> Either (Range, Error) [ ProofObligation ]
tcDecls :: InferInput -> [DeclGroup] -> Either (Range, Error) [Schema]
tcDecls InferInput
env [DeclGroup]
ds0 = case InferInput -> TcM () -> Either (Range, Error) ((), [Schema])
forall a.
InferInput -> TcM a -> Either (Range, Error) (a, [Schema])
runTcM InferInput
env ([DeclGroup] -> TcM ()
checkDecls [DeclGroup]
ds0) of
Left (Range, Error)
err -> (Range, Error) -> Either (Range, Error) [Schema]
forall a b. a -> Either a b
Left (Range, Error)
err
Right (()
_,[Schema]
ps) -> [Schema] -> Either (Range, Error) [Schema]
forall a b. b -> Either a b
Right [Schema]
ps
tcModule :: InferInput -> Module -> Either (Range, Error) [ ProofObligation ]
tcModule :: InferInput -> Module -> Either (Range, Error) [Schema]
tcModule InferInput
env Module
m = case InferInput -> TcM () -> Either (Range, Error) ((), [Schema])
forall a.
InferInput -> TcM a -> Either (Range, Error) (a, [Schema])
runTcM InferInput
env TcM ()
check of
Left (Range, Error)
err -> (Range, Error) -> Either (Range, Error) [Schema]
forall a b. a -> Either a b
Left (Range, Error)
err
Right (()
_,[Schema]
ps) -> [Schema] -> Either (Range, Error) [Schema]
forall a b. b -> Either a b
Right [Schema]
ps
where check :: TcM ()
check = (TParam -> TcM () -> TcM ()) -> TcM () -> [TParam] -> TcM ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> TcM () -> TcM ()
forall a. TParam -> TcM a -> TcM a
withTVar TcM ()
k1 ((ModTParam -> TParam) -> [ModTParam] -> [TParam]
forall a b. (a -> b) -> [a] -> [b]
map ModTParam -> TParam
mtpParam (Map Name ModTParam -> [ModTParam]
forall k a. Map k a -> [a]
Map.elems (Module -> Map Name ModTParam
forall mname. ModuleG mname -> Map Name ModTParam
mParamTypes Module
m)))
k1 :: TcM ()
k1 = (Type -> TcM () -> TcM ()) -> TcM () -> [Type] -> TcM ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> TcM () -> TcM ()
forall a. Type -> TcM a -> TcM a
withAsmp TcM ()
k2 ((Located Type -> Type) -> [Located Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Located Type -> Type
forall a. Located a -> a
thing (Module -> [Located Type]
forall mname. ModuleG mname -> [Located Type]
mParamConstraints Module
m))
k2 :: TcM ()
k2 = [(Name, Schema)] -> TcM () -> TcM ()
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars (Map Name Schema -> [(Name, Schema)]
forall k a. Map k a -> [(k, a)]
Map.toList ((ModVParam -> Schema) -> Map Name ModVParam -> Map Name Schema
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ModVParam -> Schema
mvpType (Module -> Map Name ModVParam
forall mname. ModuleG mname -> Map Name ModVParam
mParamFuns Module
m)))
(TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ [DeclGroup] -> TcM ()
checkDecls (Module -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls Module
m)
onlyNonTrivial :: [ProofObligation] -> [ProofObligation]
onlyNonTrivial :: [Schema] -> [Schema]
onlyNonTrivial = (Schema -> Bool) -> [Schema] -> [Schema]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Schema -> Bool) -> Schema -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Schema -> Bool
trivialProofObligation)
trivialProofObligation :: ProofObligation -> Bool
trivialProofObligation :: Schema -> Bool
trivialProofObligation Schema
oblig = Type -> Bool
pIsTrue Type
goal Bool -> Bool -> Bool
|| Bool
simpleEq Bool -> Bool -> Bool
|| Type
goal Type -> [Type] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type]
asmps
where
goal :: Type
goal = Schema -> Type
sType Schema
oblig
asmps :: [Type]
asmps = Schema -> [Type]
sProps Schema
oblig
simpleEq :: Bool
simpleEq = case Type -> Maybe (Type, Type)
pIsEqual Type
goal of
Just (Type
t1,Type
t2) -> Type
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t2
Maybe (Type, Type)
Nothing -> Bool
False
checkDecls :: [DeclGroup] -> TcM ()
checkDecls :: [DeclGroup] -> TcM ()
checkDecls [DeclGroup]
decls =
case [DeclGroup]
decls of
[] -> () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
DeclGroup
d : [DeclGroup]
ds -> do [(Name, Schema)]
xs <- DeclGroup -> TcM [(Name, Schema)]
checkDeclGroup DeclGroup
d
[(Name, Schema)] -> TcM () -> TcM ()
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars [(Name, Schema)]
xs ([DeclGroup] -> TcM ()
checkDecls [DeclGroup]
ds)
checkType :: Type -> TcM Kind
checkType :: Type -> TcM Kind
checkType Type
ty =
case Type
ty of
TUser Name
_ [Type]
_ Type
t -> Type -> TcM Kind
checkType Type
t
TCon TCon
tc [Type]
ts ->
do [Kind]
ks <- (Type -> TcM Kind) -> [Type] -> TcM [Kind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Type -> TcM Kind
checkType [Type]
ts
Kind -> [Kind] -> TcM Kind
checkKind (TCon -> Kind
forall t. HasKind t => t -> Kind
kindOf TCon
tc) [Kind]
ks
TNewtype Newtype
nt [Type]
ts ->
do [Kind]
ks <- (Type -> TcM Kind) -> [Type] -> TcM [Kind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Type -> TcM Kind
checkType [Type]
ts
Kind -> [Kind] -> TcM Kind
checkKind (Newtype -> Kind
forall t. HasKind t => t -> Kind
kindOf Newtype
nt) [Kind]
ks
TVar TVar
tv -> TVar -> TcM Kind
lookupTVar TVar
tv
TRec RecordMap Ident Type
fs ->
do RecordMap Ident Type -> (Type -> TcM ()) -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ RecordMap Ident Type
fs ((Type -> TcM ()) -> TcM ()) -> (Type -> TcM ()) -> TcM ()
forall a b. (a -> b) -> a -> b
$ \Type
t ->
do Kind
k <- Type -> TcM Kind
checkType Type
t
Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KType) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Error -> TcM ()
forall a. Error -> TcM a
reportError (Error -> TcM ()) -> Error -> TcM ()
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> Error
KindMismatch Kind
KType Kind
k
Kind -> TcM Kind
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
KType
where
checkKind :: Kind -> [Kind] -> TcM Kind
checkKind Kind
k [] = case Kind
k of
Kind
_ :-> Kind
_ -> Error -> TcM Kind
forall a. Error -> TcM a
reportError (Error -> TcM Kind) -> Error -> TcM Kind
forall a b. (a -> b) -> a -> b
$ Kind -> Error
NotEnoughArgumentsInKind Kind
k
Kind
KProp -> Kind -> TcM Kind
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
Kind
KNum -> Kind -> TcM Kind
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
Kind
KType -> Kind -> TcM Kind
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
checkKind (Kind
k1 :-> Kind
k2) (Kind
k : [Kind]
ks)
| Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k1 = Kind -> [Kind] -> TcM Kind
checkKind Kind
k2 [Kind]
ks
| Bool
otherwise = Error -> TcM Kind
forall a. Error -> TcM a
reportError (Error -> TcM Kind) -> Error -> TcM Kind
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> Error
KindMismatch Kind
k1 Kind
k
checkKind Kind
k [Kind]
ks = Error -> TcM Kind
forall a. Error -> TcM a
reportError (Error -> TcM Kind) -> Error -> TcM Kind
forall a b. (a -> b) -> a -> b
$ Kind -> [Kind] -> Error
BadTypeApplication Kind
k [Kind]
ks
checkTypeIs :: Kind -> Type -> TcM ()
checkTypeIs :: Kind -> Type -> TcM ()
checkTypeIs Kind
k Type
ty =
do Kind
k1 <- Type -> TcM Kind
checkType Type
ty
Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k1) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Error -> TcM ()
forall a. Error -> TcM a
reportError (Error -> TcM ()) -> Error -> TcM ()
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> Error
KindMismatch Kind
k Kind
k1
checkSchema :: Schema -> TcM ()
checkSchema :: Schema -> TcM ()
checkSchema (Forall [TParam]
as [Type]
ps Type
t) = (TParam -> TcM () -> TcM ()) -> TcM () -> [TParam] -> TcM ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> TcM () -> TcM ()
forall a. TParam -> TcM a -> TcM a
withTVar TcM ()
check [TParam]
as
where check :: TcM ()
check = do (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Kind -> Type -> TcM ()
checkTypeIs Kind
KProp) [Type]
ps
Kind -> Type -> TcM ()
checkTypeIs Kind
KType Type
t
data AreSame = SameIf [Prop]
| NotSame
areSame :: AreSame
areSame :: AreSame
areSame = [Type] -> AreSame
SameIf []
sameAnd :: AreSame -> AreSame -> AreSame
sameAnd :: AreSame -> AreSame -> AreSame
sameAnd AreSame
x AreSame
y =
case (AreSame
x,AreSame
y) of
(SameIf [Type]
xs, SameIf [Type]
ys) -> [Type] -> AreSame
SameIf ([Type]
xs [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
ys)
(AreSame, AreSame)
_ -> AreSame
NotSame
sameBool :: Bool -> AreSame
sameBool :: Bool -> AreSame
sameBool Bool
b = if Bool
b then AreSame
areSame else AreSame
NotSame
sameTypes :: String -> Type -> Type -> TcM ()
sameTypes :: String -> Type -> Type -> TcM ()
sameTypes String
msg Type
x Type
y = String -> Schema -> Schema -> TcM ()
sameSchemas String
msg (Type -> Schema
tMono Type
x) (Type -> Schema
tMono Type
y)
sameSchemas :: String -> Schema -> Schema -> TcM ()
sameSchemas :: String -> Schema -> Schema -> TcM ()
sameSchemas String
msg Schema
x Schema
y =
case Schema -> Schema -> AreSame
forall a. Same a => a -> a -> AreSame
same Schema
x Schema
y of
AreSame
NotSame -> Error -> TcM ()
forall a. Error -> TcM a
reportError (String -> Schema -> Schema -> Error
TypeMismatch String
msg Schema
x Schema
y)
SameIf [Type]
ps -> (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> TcM ()
proofObligation [Type]
ps
class Same a where
same :: a -> a -> AreSame
instance Same a => Same [a] where
same :: [a] -> [a] -> AreSame
same [] [] = AreSame
areSame
same (a
x : [a]
xs) (a
y : [a]
ys) = a -> a -> AreSame
forall a. Same a => a -> a -> AreSame
same a
x a
y AreSame -> AreSame -> AreSame
`sameAnd` [a] -> [a] -> AreSame
forall a. Same a => a -> a -> AreSame
same [a]
xs [a]
ys
same [a]
_ [a]
_ = AreSame
NotSame
data Field a b = Field a b
instance (Eq a, Same b) => Same (Field a b) where
same :: Field a b -> Field a b -> AreSame
same (Field a
x b
a) (Field a
y b
b) = Bool -> AreSame
sameBool (a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y) AreSame -> AreSame -> AreSame
`sameAnd` b -> b -> AreSame
forall a. Same a => a -> a -> AreSame
same b
a b
b
instance Same Type where
same :: Type -> Type -> AreSame
same Type
t1 Type
t2
| Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
k2 = AreSame
NotSame
| Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KNum = if Type
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t2 then [Type] -> AreSame
SameIf [] else [Type] -> AreSame
SameIf [ Type
t1 Type -> Type -> Type
=#= Type
t2 ]
| Bool
otherwise =
case (Type -> Type
tNoUser Type
t1, Type -> Type
tNoUser Type
t2) of
(TVar TVar
x, TVar TVar
y) -> Bool -> AreSame
sameBool (TVar
x TVar -> TVar -> Bool
forall a. Eq a => a -> a -> Bool
== TVar
y)
(TRec RecordMap Ident Type
x, TRec RecordMap Ident Type
y) -> [Field Ident Type] -> [Field Ident Type] -> AreSame
forall a. Same a => a -> a -> AreSame
same (RecordMap Ident Type -> [Field Ident Type]
forall {a} {b}. RecordMap a b -> [Field a b]
mkRec RecordMap Ident Type
x) (RecordMap Ident Type -> [Field Ident Type]
forall {a} {b}. RecordMap a b -> [Field a b]
mkRec RecordMap Ident Type
y)
(TNewtype Newtype
x [Type]
xs, TNewtype Newtype
y [Type]
ys) -> Field Newtype [Type] -> Field Newtype [Type] -> AreSame
forall a. Same a => a -> a -> AreSame
same (Newtype -> [Type] -> Field Newtype [Type]
forall a b. a -> b -> Field a b
Field Newtype
x [Type]
xs) (Newtype -> [Type] -> Field Newtype [Type]
forall a b. a -> b -> Field a b
Field Newtype
y [Type]
ys)
(TCon TCon
x [Type]
xs, TCon TCon
y [Type]
ys) -> Field TCon [Type] -> Field TCon [Type] -> AreSame
forall a. Same a => a -> a -> AreSame
same (TCon -> [Type] -> Field TCon [Type]
forall a b. a -> b -> Field a b
Field TCon
x [Type]
xs) (TCon -> [Type] -> Field TCon [Type]
forall a b. a -> b -> Field a b
Field TCon
y [Type]
ys)
(Type, Type)
_ -> AreSame
NotSame
where
k1 :: Kind
k1 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t1
k2 :: Kind
k2 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t2
mkRec :: RecordMap a b -> [Field a b]
mkRec RecordMap a b
r = [ a -> b -> Field a b
forall a b. a -> b -> Field a b
Field a
x b
y | (a
x,b
y) <- RecordMap a b -> [(a, b)]
forall a b. RecordMap a b -> [(a, b)]
canonicalFields RecordMap a b
r ]
instance Same Schema where
same :: Schema -> Schema -> AreSame
same (Forall [TParam]
xs [Type]
ps Type
s) (Forall [TParam]
ys [Type]
qs Type
t) =
[TParam] -> [TParam] -> AreSame
forall a. Same a => a -> a -> AreSame
same [TParam]
xs [TParam]
ys AreSame -> AreSame -> AreSame
`sameAnd` [Type] -> [Type] -> AreSame
forall a. Same a => a -> a -> AreSame
same [Type]
ps [Type]
qs AreSame -> AreSame -> AreSame
`sameAnd` Type -> Type -> AreSame
forall a. Same a => a -> a -> AreSame
same Type
s Type
t
instance Same TParam where
same :: TParam -> TParam -> AreSame
same TParam
x TParam
y = Bool -> AreSame
sameBool (TParam -> Maybe Name
tpName TParam
x Maybe Name -> Maybe Name -> Bool
forall a. Eq a => a -> a -> Bool
== TParam -> Maybe Name
tpName TParam
y Bool -> Bool -> Bool
&& TParam -> Kind
tpKind TParam
x Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== TParam -> Kind
tpKind TParam
y)
exprType :: Expr -> TcM Type
exprType :: Expr -> TcM Type
exprType Expr
expr =
do Schema
s <- Expr -> TcM Schema
exprSchema Expr
expr
case Schema -> Maybe Type
isMono Schema
s of
Just Type
t -> Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
Maybe Type
Nothing -> Error -> TcM Type
forall a. Error -> TcM a
reportError (Schema -> Error
ExpectedMono Schema
s)
exprSchema :: Expr -> TcM Schema
exprSchema :: Expr -> TcM Schema
exprSchema Expr
expr =
case Expr
expr of
ELocated Range
rng Expr
t -> Range -> TcM Schema -> TcM Schema
forall a. Range -> TcM a -> TcM a
withRange Range
rng (Expr -> TcM Schema
exprSchema Expr
t)
EList [Expr]
es Type
t ->
do Kind -> Type -> TcM ()
checkTypeIs Kind
KType Type
t
[Expr] -> (Expr -> TcM ()) -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Expr]
es ((Expr -> TcM ()) -> TcM ()) -> (Expr -> TcM ()) -> TcM ()
forall a b. (a -> b) -> a -> b
$ \Expr
e ->
do Type
t1 <- Expr -> TcM Type
exprType Expr
e
String -> Type -> Type -> TcM ()
sameTypes String
"EList" Type
t1 Type
t
Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> TcM Schema) -> Schema -> TcM Schema
forall a b. (a -> b) -> a -> b
$ Type -> Schema
tMono (Type -> Schema) -> Type -> Schema
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
tSeq (Int -> Type
forall a. Integral a => a -> Type
tNum ([Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es)) Type
t
ETuple [Expr]
es ->
([Type] -> Schema) -> TcM [Type] -> TcM Schema
forall a b. (a -> b) -> TcM a -> TcM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type -> Schema
tMono (Type -> Schema) -> ([Type] -> Type) -> [Type] -> Schema
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type] -> Type
tTuple) ((Expr -> TcM Type) -> [Expr] -> TcM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Expr -> TcM Type
exprType [Expr]
es)
ERec RecordMap Ident Expr
fs ->
do RecordMap Ident Type
fs1 <- (Expr -> TcM Type)
-> RecordMap Ident Expr -> TcM (RecordMap Ident Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
traverse Expr -> TcM Type
exprType RecordMap Ident Expr
fs
Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> TcM Schema) -> Schema -> TcM Schema
forall a b. (a -> b) -> a -> b
$ Type -> Schema
tMono (Type -> Schema) -> Type -> Schema
forall a b. (a -> b) -> a -> b
$ RecordMap Ident Type -> Type
TRec RecordMap Ident Type
fs1
ESet Type
_ Expr
e Selector
x Expr
v ->
do Type
ty <- Expr -> TcM Type
exprType Expr
e
Type
expe <- Type -> Selector -> TcM Type
checkHas Type
ty Selector
x
Type
has <- Expr -> TcM Type
exprType Expr
v
String -> Type -> Type -> TcM ()
sameTypes String
"ESet" Type
expe Type
has
Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Schema
tMono Type
ty)
ESel Expr
e Selector
sel -> do Type
ty <- Expr -> TcM Type
exprType Expr
e
Type
ty1 <- Type -> Selector -> TcM Type
checkHas Type
ty Selector
sel
Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Schema
tMono Type
ty1)
EIf Expr
e1 Expr
e2 Expr
e3 ->
do Type
ty <- Expr -> TcM Type
exprType Expr
e1
String -> Type -> Type -> TcM ()
sameTypes String
"EIf_condition" Type
tBit Type
ty
Type
t1 <- Expr -> TcM Type
exprType Expr
e2
Type
t2 <- Expr -> TcM Type
exprType Expr
e3
String -> Type -> Type -> TcM ()
sameTypes String
"EIf_arms" Type
t1 Type
t2
Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> TcM Schema) -> Schema -> TcM Schema
forall a b. (a -> b) -> a -> b
$ Type -> Schema
tMono Type
t1
EComp Type
len Type
t Expr
e [[Match]]
mss ->
do Kind -> Type -> TcM ()
checkTypeIs Kind
KNum Type
len
Kind -> Type -> TcM ()
checkTypeIs Kind
KType Type
t
([[(Name, Schema)]]
xs,[Type]
ls) <- [([(Name, Schema)], Type)] -> ([[(Name, Schema)]], [Type])
forall a b. [(a, b)] -> ([a], [b])
unzip ([([(Name, Schema)], Type)] -> ([[(Name, Schema)]], [Type]))
-> TcM [([(Name, Schema)], Type)]
-> TcM ([[(Name, Schema)]], [Type])
forall a b. (a -> b) -> TcM a -> TcM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ([Match] -> TcM ([(Name, Schema)], Type))
-> [[Match]] -> TcM [([(Name, Schema)], Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM [Match] -> TcM ([(Name, Schema)], Type)
checkArm [[Match]]
mss
Type
elT <- [(Name, Schema)] -> TcM Type -> TcM Type
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars ([[(Name, Schema)]] -> [(Name, Schema)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Name, Schema)]]
xs) (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$ Expr -> TcM Type
exprType Expr
e
case [Type]
ls of
[] -> () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
[Type]
_ -> Type -> Type -> TcM ()
convertible (Type -> Type -> Type
tSeq Type
len Type
t) (Type -> Type -> Type
tSeq ((Type -> Type -> Type) -> [Type] -> Type
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
tMin [Type]
ls) Type
elT)
Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Schema
tMono (Type -> Type -> Type
tSeq Type
len Type
t))
EVar Name
x -> Name -> TcM Schema
lookupVar Name
x
ETAbs TParam
a Expr
e ->
do Forall [TParam]
as [Type]
p Type
t <- TParam -> TcM Schema -> TcM Schema
forall a. TParam -> TcM a -> TcM a
withTVar TParam
a (Expr -> TcM Schema
exprSchema Expr
e)
Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((TParam -> Bool) -> [TParam] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TParam -> TParam -> Bool
forall a. Eq a => a -> a -> Bool
== TParam
a) [TParam]
as) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
Error -> TcM ()
forall a. Error -> TcM a
reportError (Error -> TcM ()) -> Error -> TcM ()
forall a b. (a -> b) -> a -> b
$ TParam -> Error
RepeatedVariableInForall TParam
a
Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TParam] -> [Type] -> Type -> Schema
Forall (TParam
a TParam -> [TParam] -> [TParam]
forall a. a -> [a] -> [a]
: [TParam]
as) [Type]
p Type
t)
ETApp Expr
e Type
t ->
do Kind
k <- Type -> TcM Kind
checkType Type
t
Schema
s <- Expr -> TcM Schema
exprSchema Expr
e
case Schema
s of
Forall (TParam
a : [TParam]
as) [Type]
ps Type
t1 ->
do let vs :: Set TVar
vs = Type -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Type
t
[TVar] -> (TVar -> TcM ()) -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ((TParam -> TVar) -> [TParam] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar [TParam]
as) ((TVar -> TcM ()) -> TcM ()) -> (TVar -> TcM ()) -> TcM ()
forall a b. (a -> b) -> a -> b
$ \TVar
b ->
Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TVar
b TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
vs) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Error -> TcM ()
forall a. Error -> TcM a
reportError (Error -> TcM ()) -> Error -> TcM ()
forall a b. (a -> b) -> a -> b
$ TVar -> Error
Captured TVar
b
let k' :: Kind
k' = TParam -> Kind
forall t. HasKind t => t -> Kind
kindOf TParam
a
Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k') (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Error -> TcM ()
forall a. Error -> TcM a
reportError (Error -> TcM ()) -> Error -> TcM ()
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> Error
KindMismatch Kind
k' Kind
k
let su :: Subst
su = TParam -> Type -> Subst
singleTParamSubst TParam
a Type
t
Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> TcM Schema) -> Schema -> TcM Schema
forall a b. (a -> b) -> a -> b
$ [TParam] -> [Type] -> Type -> Schema
Forall [TParam]
as (Subst -> [Type] -> [Type]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Type]
ps) (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t1)
Forall [] [Type]
_ Type
_ -> Error -> TcM Schema
forall a. Error -> TcM a
reportError Error
BadInstantiation
EApp Expr
e1 Expr
e2 ->
do Type
t1 <- Expr -> TcM Type
exprType Expr
e1
Type
t2 <- Expr -> TcM Type
exprType Expr
e2
case Type -> Type
tNoUser Type
t1 of
TCon (TC TC
TCFun) [ Type
a, Type
b ]
| SameIf [Type]
ps <- Type -> Type -> AreSame
forall a. Same a => a -> a -> AreSame
same Type
a Type
t2 ->
do (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> TcM ()
proofObligation [Type]
ps
Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Schema
tMono Type
b)
Type
tf -> Error -> TcM Schema
forall a. Error -> TcM a
reportError (Type -> Type -> Error
BadApplication Type
tf Type
t1)
EAbs Name
x Type
t Expr
e ->
do Kind -> Type -> TcM ()
checkTypeIs Kind
KType Type
t
Type
res <- Name -> Type -> TcM Type -> TcM Type
forall a. Name -> Type -> TcM a -> TcM a
withVar Name
x Type
t (Expr -> TcM Type
exprType Expr
e)
Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> TcM Schema) -> Schema -> TcM Schema
forall a b. (a -> b) -> a -> b
$ Type -> Schema
tMono (Type -> Schema) -> Type -> Schema
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
tFun Type
t Type
res
EProofAbs Type
p Expr
e ->
do Kind -> Type -> TcM ()
checkTypeIs Kind
KProp Type
p
Type -> TcM Schema -> TcM Schema
forall a. Type -> TcM a -> TcM a
withAsmp Type
p (TcM Schema -> TcM Schema) -> TcM Schema -> TcM Schema
forall a b. (a -> b) -> a -> b
$ do Forall [TParam]
as [Type]
ps Type
t <- Expr -> TcM Schema
exprSchema Expr
e
Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Schema -> TcM Schema) -> Schema -> TcM Schema
forall a b. (a -> b) -> a -> b
$ [TParam] -> [Type] -> Type -> Schema
Forall [TParam]
as (Type
p Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ps) Type
t
EProofApp Expr
e ->
do Forall [TParam]
as [Type]
ps Type
t <- Expr -> TcM Schema
exprSchema Expr
e
case ([TParam]
as,[Type]
ps) of
([], Type
p:[Type]
qs) -> do Type -> TcM ()
proofObligation Type
p
Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TParam] -> [Type] -> Type -> Schema
Forall [] [Type]
qs Type
t)
([], [Type]
_) -> Error -> TcM Schema
forall a. Error -> TcM a
reportError Error
BadProofNoAbs
([TParam]
_,[Type]
_) -> Error -> TcM Schema
forall a. Error -> TcM a
reportError ([TParam] -> Error
BadProofTyVars [TParam]
as)
EWhere Expr
e [DeclGroup]
dgs ->
let go :: [DeclGroup] -> TcM Schema
go [] = Expr -> TcM Schema
exprSchema Expr
e
go (DeclGroup
d : [DeclGroup]
ds) = do [(Name, Schema)]
xs <- DeclGroup -> TcM [(Name, Schema)]
checkDeclGroup DeclGroup
d
[(Name, Schema)] -> TcM Schema -> TcM Schema
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars [(Name, Schema)]
xs ([DeclGroup] -> TcM Schema
go [DeclGroup]
ds)
in [DeclGroup] -> TcM Schema
go [DeclGroup]
dgs
EPropGuards [([Type], Expr)]
_guards Type
typ ->
Schema -> TcM Schema
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Forall {sVars :: [TParam]
sVars = [], sProps :: [Type]
sProps = [], sType :: Type
sType = Type
typ}
checkHas :: Type -> Selector -> TcM Type
checkHas :: Type -> Selector -> TcM Type
checkHas Type
t Selector
sel =
case Selector
sel of
TupleSel Int
n Maybe Int
mb ->
case Type -> Type
tNoUser Type
t of
TCon (TC (TCTuple Int
sz)) [Type]
ts ->
do case Maybe Int
mb of
Just Int
sz1 ->
Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
sz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
sz1) (Error -> TcM ()
forall a. Error -> TcM a
reportError (Int -> Int -> Error
UnexpectedTupleShape Int
sz1 Int
sz))
Maybe Int
Nothing -> () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
sz) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Error -> TcM ()
forall a. Error -> TcM a
reportError (Int -> Int -> Error
TupleSelectorOutOfRange Int
n Int
sz)
Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TcM Type) -> Type -> TcM Type
forall a b. (a -> b) -> a -> b
$ [Type]
ts [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
n
TCon (TC TC
TCSeq) [Type
s,Type
elT] ->
do Type
res <- Type -> Selector -> TcM Type
checkHas Type
elT Selector
sel
Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCSeq) [Type
s,Type
res])
TCon (TC TC
TCFun) [Type
a,Type
b] ->
do Type
res <- Type -> Selector -> TcM Type
checkHas Type
b Selector
sel
Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCFun) [Type
a,Type
res])
Type
_ -> Error -> TcM Type
forall a. Error -> TcM a
reportError (Error -> TcM Type) -> Error -> TcM Type
forall a b. (a -> b) -> a -> b
$ Selector -> Type -> Error
BadSelector Selector
sel Type
t
RecordSel Ident
f Maybe [Ident]
mb ->
case Type -> Type
tNoUser Type
t of
TRec RecordMap Ident Type
fs ->
do case Maybe [Ident]
mb of
Maybe [Ident]
Nothing -> () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just [Ident]
fs1 ->
do let ns :: [Ident]
ns = Set Ident -> [Ident]
forall a. Set a -> [a]
Set.toList (RecordMap Ident Type -> Set Ident
forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Type
fs)
ns1 :: [Ident]
ns1 = [Ident] -> [Ident]
forall a. Ord a => [a] -> [a]
sort [Ident]
fs1
Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Ident]
ns [Ident] -> [Ident] -> Bool
forall a. Eq a => a -> a -> Bool
== [Ident]
ns1) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
Error -> TcM ()
forall a. Error -> TcM a
reportError (Error -> TcM ()) -> Error -> TcM ()
forall a b. (a -> b) -> a -> b
$ [Ident] -> [Ident] -> Error
UnexpectedRecordShape [Ident]
ns1 [Ident]
ns
case Ident -> RecordMap Ident Type -> Maybe Type
forall a b. Ord a => a -> RecordMap a b -> Maybe b
lookupField Ident
f RecordMap Ident Type
fs of
Maybe Type
Nothing -> Error -> TcM Type
forall a. Error -> TcM a
reportError (Error -> TcM Type) -> Error -> TcM Type
forall a b. (a -> b) -> a -> b
$ Ident -> [Ident] -> Error
MissingField Ident
f ([Ident] -> Error) -> [Ident] -> Error
forall a b. (a -> b) -> a -> b
$ RecordMap Ident Type -> [Ident]
forall a b. RecordMap a b -> [a]
displayOrder RecordMap Ident Type
fs
Just Type
ft -> Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ft
TCon (TC TC
TCSeq) [Type
s,Type
elT] -> do Type
res <- Type -> Selector -> TcM Type
checkHas Type
elT Selector
sel
Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCSeq) [Type
s,Type
res])
TCon (TC TC
TCFun) [Type
a,Type
b] -> do Type
res <- Type -> Selector -> TcM Type
checkHas Type
b Selector
sel
Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCFun) [Type
a,Type
res])
Type
_ -> Error -> TcM Type
forall a. Error -> TcM a
reportError (Error -> TcM Type) -> Error -> TcM Type
forall a b. (a -> b) -> a -> b
$ Selector -> Type -> Error
BadSelector Selector
sel Type
t
ListSel Int
_ Maybe Int
mb ->
case Type -> Type
tNoUser Type
t of
TCon (TC TC
TCSeq) [ Type
n, Type
elT ] ->
do case Maybe Int
mb of
Maybe Int
Nothing -> () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just Int
len ->
case Type -> Type
tNoUser Type
n of
TCon (TC (TCNum Integer
m)) []
| Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
len -> () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Type
_ -> Error -> TcM ()
forall a. Error -> TcM a
reportError (Error -> TcM ()) -> Error -> TcM ()
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Error
UnexpectedSequenceShape Int
len Type
n
Type -> TcM Type
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
elT
Type
_ -> Error -> TcM Type
forall a. Error -> TcM a
reportError (Error -> TcM Type) -> Error -> TcM Type
forall a b. (a -> b) -> a -> b
$ Selector -> Type -> Error
BadSelector Selector
sel Type
t
convertible :: Type -> Type -> TcM ()
convertible :: Type -> Type -> TcM ()
convertible Type
t1 Type
t2
| Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
k2 = Error -> TcM ()
forall a. Error -> TcM a
reportError (Kind -> Kind -> Error
KindMismatch Kind
k1 Kind
k2)
| Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KNum = Type -> TcM ()
proofObligation (Type
t1 Type -> Type -> Type
=#= Type
t2)
where
k1 :: Kind
k1 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t1
k2 :: Kind
k2 = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t2
convertible Type
t1 Type
t2 = Type -> Type -> TcM ()
go Type
t1 Type
t2
where
go :: Type -> Type -> TcM ()
go Type
ty1 Type
ty2 =
let err :: TcM a
err = Error -> TcM a
forall a. Error -> TcM a
reportError (Error -> TcM a) -> Error -> TcM a
forall a b. (a -> b) -> a -> b
$ String -> Schema -> Schema -> Error
TypeMismatch String
"convertible" (Type -> Schema
tMono Type
ty1) (Type -> Schema
tMono Type
ty2)
other :: Type
other = Type -> Type
tNoUser Type
ty2
goMany :: [Type] -> [Type] -> TcM ()
goMany [] [] = () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
goMany (Type
x : [Type]
xs) (Type
y : [Type]
ys) = Type -> Type -> TcM ()
convertible Type
x Type
y TcM () -> TcM () -> TcM ()
forall a b. TcM a -> TcM b -> TcM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Type] -> [Type] -> TcM ()
goMany [Type]
xs [Type]
ys
goMany [Type]
_ [Type]
_ = TcM ()
forall {a}. TcM a
err
in case Type
ty1 of
TUser Name
_ [Type]
_ Type
s -> Type -> Type -> TcM ()
go Type
s Type
ty2
TVar TVar
x -> case Type
other of
TVar TVar
y | TVar
x TVar -> TVar -> Bool
forall a. Eq a => a -> a -> Bool
== TVar
y -> () -> TcM ()
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Type
_ -> TcM ()
forall {a}. TcM a
err
TCon TCon
tc1 [Type]
ts1 -> case Type
other of
TCon TCon
tc2 [Type]
ts2
| TCon
tc1 TCon -> TCon -> Bool
forall a. Eq a => a -> a -> Bool
== TCon
tc2 -> [Type] -> [Type] -> TcM ()
goMany [Type]
ts1 [Type]
ts2
Type
_ -> TcM ()
forall {a}. TcM a
err
TNewtype Newtype
nt1 [Type]
ts1 ->
case Type
other of
TNewtype Newtype
nt2 [Type]
ts2
| Newtype
nt1 Newtype -> Newtype -> Bool
forall a. Eq a => a -> a -> Bool
== Newtype
nt2 -> [Type] -> [Type] -> TcM ()
goMany [Type]
ts1 [Type]
ts2
Type
_ -> TcM ()
forall {a}. TcM a
err
TRec RecordMap Ident Type
fs ->
case Type
other of
TRec RecordMap Ident Type
gs ->
do Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (RecordMap Ident Type -> Set Ident
forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Type
fs Set Ident -> Set Ident -> Bool
forall a. Eq a => a -> a -> Bool
== RecordMap Ident Type -> Set Ident
forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Type
gs) TcM ()
forall {a}. TcM a
err
[Type] -> [Type] -> TcM ()
goMany (RecordMap Ident Type -> [Type]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs) (RecordMap Ident Type -> [Type]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
gs)
Type
_ -> TcM ()
forall {a}. TcM a
err
checkDecl :: Bool -> Decl -> TcM (Name, Schema)
checkDecl :: Bool -> Decl -> TcM (Name, Schema)
checkDecl Bool
checkSig Decl
d =
case Decl -> DeclDef
dDefinition Decl
d of
DeclDef
DPrim ->
do Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkSig (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Schema -> TcM ()
checkSchema (Schema -> TcM ()) -> Schema -> TcM ()
forall a b. (a -> b) -> a -> b
$ Decl -> Schema
dSignature Decl
d
(Name, Schema) -> TcM (Name, Schema)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Name
dName Decl
d, Decl -> Schema
dSignature Decl
d)
DForeign FFIFunType
_ ->
do Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkSig (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Schema -> TcM ()
checkSchema (Schema -> TcM ()) -> Schema -> TcM ()
forall a b. (a -> b) -> a -> b
$ Decl -> Schema
dSignature Decl
d
(Name, Schema) -> TcM (Name, Schema)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Name
dName Decl
d, Decl -> Schema
dSignature Decl
d)
DExpr Expr
e ->
do let s :: Schema
s = Decl -> Schema
dSignature Decl
d
Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkSig (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ Schema -> TcM ()
checkSchema Schema
s
Schema
s1 <- Expr -> TcM Schema
exprSchema Expr
e
let nm :: Name
nm = Decl -> Name
dName Decl
d
loc :: String
loc = String
"definition of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
forall a. PP a => a -> Doc
pp Name
nm) String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
", at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Range -> Doc
forall a. PP a => a -> Doc
pp (Name -> Range
nameLoc Name
nm))
String -> Schema -> Schema -> TcM ()
sameSchemas String
loc Schema
s Schema
s1
(Name, Schema) -> TcM (Name, Schema)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Name
dName Decl
d, Schema
s)
checkDeclGroup :: DeclGroup -> TcM [(Name, Schema)]
checkDeclGroup :: DeclGroup -> TcM [(Name, Schema)]
checkDeclGroup DeclGroup
dg =
case DeclGroup
dg of
NonRecursive Decl
d -> do (Name, Schema)
x <- Bool -> Decl -> TcM (Name, Schema)
checkDecl Bool
True Decl
d
[(Name, Schema)] -> TcM [(Name, Schema)]
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, Schema)
x]
Recursive [Decl]
ds ->
do [(Name, Schema)]
xs <- [Decl] -> (Decl -> TcM (Name, Schema)) -> TcM [(Name, Schema)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Decl]
ds ((Decl -> TcM (Name, Schema)) -> TcM [(Name, Schema)])
-> (Decl -> TcM (Name, Schema)) -> TcM [(Name, Schema)]
forall a b. (a -> b) -> a -> b
$ \Decl
d ->
do Schema -> TcM ()
checkSchema (Decl -> Schema
dSignature Decl
d)
(Name, Schema) -> TcM (Name, Schema)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Name
dName Decl
d, Decl -> Schema
dSignature Decl
d)
[(Name, Schema)] -> TcM [(Name, Schema)] -> TcM [(Name, Schema)]
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars [(Name, Schema)]
xs (TcM [(Name, Schema)] -> TcM [(Name, Schema)])
-> TcM [(Name, Schema)] -> TcM [(Name, Schema)]
forall a b. (a -> b) -> a -> b
$ (Decl -> TcM (Name, Schema)) -> [Decl] -> TcM [(Name, Schema)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool -> Decl -> TcM (Name, Schema)
checkDecl Bool
False) [Decl]
ds
checkMatch :: Match -> TcM ((Name, Schema), Type)
checkMatch :: Match -> TcM ((Name, Schema), Type)
checkMatch Match
ma =
case Match
ma of
From Name
x Type
len Type
elt Expr
e ->
do Kind -> Type -> TcM ()
checkTypeIs Kind
KNum Type
len
Kind -> Type -> TcM ()
checkTypeIs Kind
KType Type
elt
Type
t1 <- Expr -> TcM Type
exprType Expr
e
case Type -> Type
tNoUser Type
t1 of
TCon (TC TC
TCSeq) [ Type
l, Type
el ]
| SameIf [Type]
ps <- Type -> Type -> AreSame
forall a. Same a => a -> a -> AreSame
same Type
elt Type
el ->
do (Type -> TcM ()) -> [Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> TcM ()
proofObligation [Type]
ps
((Name, Schema), Type) -> TcM ((Name, Schema), Type)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
x, Type -> Schema
tMono Type
elt), Type
l)
| Bool
otherwise -> Error -> TcM ((Name, Schema), Type)
forall a. Error -> TcM a
reportError (Error -> TcM ((Name, Schema), Type))
-> Error -> TcM ((Name, Schema), Type)
forall a b. (a -> b) -> a -> b
$ String -> Schema -> Schema -> Error
TypeMismatch String
"From" (Type -> Schema
tMono Type
elt) (Type -> Schema
tMono Type
el)
Type
_ -> Error -> TcM ((Name, Schema), Type)
forall a. Error -> TcM a
reportError (Error -> TcM ((Name, Schema), Type))
-> Error -> TcM ((Name, Schema), Type)
forall a b. (a -> b) -> a -> b
$ Type -> Error
BadMatch Type
t1
Let Decl
d -> do (Name, Schema)
x <- Bool -> Decl -> TcM (Name, Schema)
checkDecl Bool
True Decl
d
((Name, Schema), Type) -> TcM ((Name, Schema), Type)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name, Schema)
x, Int -> Type
forall a. Integral a => a -> Type
tNum (Int
1 :: Int))
checkArm :: [Match] -> TcM ([(Name, Schema)], Type)
checkArm :: [Match] -> TcM ([(Name, Schema)], Type)
checkArm [] = Error -> TcM ([(Name, Schema)], Type)
forall a. Error -> TcM a
reportError Error
EmptyArm
checkArm [Match
m] = do ((Name, Schema)
x,Type
l) <- Match -> TcM ((Name, Schema), Type)
checkMatch Match
m
([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Schema)
x], Type
l)
checkArm (Match
m : [Match]
ms) =
do ((Name, Schema)
x, Type
l) <- Match -> TcM ((Name, Schema), Type)
checkMatch Match
m
([(Name, Schema)]
xs, Type
l1) <- [(Name, Schema)]
-> TcM ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type)
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars [(Name, Schema)
x] (TcM ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type))
-> TcM ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type)
forall a b. (a -> b) -> a -> b
$ [Match] -> TcM ([(Name, Schema)], Type)
checkArm [Match]
ms
let newLen :: Type
newLen = Type -> Type -> Type
tMul Type
l Type
l1
([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type))
-> ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type)
forall a b. (a -> b) -> a -> b
$ if (Name, Schema) -> Name
forall a b. (a, b) -> a
fst (Name, Schema)
x Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Name, Schema) -> Name) -> [(Name, Schema)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Schema) -> Name
forall a b. (a, b) -> a
fst [(Name, Schema)]
xs
then ([(Name, Schema)]
xs, Type
newLen)
else ((Name, Schema)
x (Name, Schema) -> [(Name, Schema)] -> [(Name, Schema)]
forall a. a -> [a] -> [a]
: [(Name, Schema)]
xs, Type
newLen)
data RO = RO
{ RO -> Map Int TParam
roTVars :: Map Int TParam
, RO -> [Type]
roAsmps :: [Prop]
, RO -> Range
roRange :: Range
, RO -> Map Name Schema
roVars :: Map Name Schema
}
type ProofObligation = Schema
data RW = RW
{ RW -> [Schema]
woProofObligations :: [ProofObligation]
}
newtype TcM a = TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a)
instance Functor TcM where
fmap :: forall a b. (a -> b) -> TcM a -> TcM b
fmap = (a -> b) -> TcM a -> TcM b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM
instance A.Applicative TcM where
pure :: forall a. a -> TcM a
pure a
a = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (a -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall a.
a -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a)
<*> :: forall a b. TcM (a -> b) -> TcM a -> TcM b
(<*>) = TcM (a -> b) -> TcM a -> TcM b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad TcM where
return :: forall a. a -> TcM a
return = a -> TcM a
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m >>= :: forall a b. TcM a -> (a -> TcM b) -> TcM b
>>= a -> TcM b
f = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) b -> TcM b
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (do a
a <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m
let TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) b
m1 = a -> TcM b
f a
a
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) b
m1)
runTcM :: InferInput -> TcM a -> Either (Range, Error) (a, [ProofObligation])
runTcM :: forall a.
InferInput -> TcM a -> Either (Range, Error) (a, [Schema])
runTcM InferInput
env (TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m) =
case ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> RO -> RW -> (Either (Range, Error) a, RW)
forall (m :: * -> *) a r. RunM m a r => m a -> r
runM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m RO
ro RW
rw of
(Left (Range, Error)
err, RW
_) -> (Range, Error) -> Either (Range, Error) (a, [Schema])
forall a b. a -> Either a b
Left (Range, Error)
err
(Right a
a, RW
s) -> (a, [Schema]) -> Either (Range, Error) (a, [Schema])
forall a b. b -> Either a b
Right (a
a, RW -> [Schema]
woProofObligations RW
s)
where
allPs :: ModParamNames
allPs = InferInput -> ModParamNames
inpParams InferInput
env
ro :: RO
ro = RO { roTVars :: Map Int TParam
roTVars = [(Int, TParam)] -> Map Int TParam
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (TParam -> Int
tpUnique TParam
x, TParam
x)
| ModTParam
tp <- Map Name ModTParam -> [ModTParam]
forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
allPs)
, let x :: TParam
x = ModTParam -> TParam
mtpParam ModTParam
tp ]
, roAsmps :: [Type]
roAsmps = (Located Type -> Type) -> [Located Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Located Type -> Type
forall a. Located a -> a
thing (ModParamNames -> [Located Type]
mpnConstraints ModParamNames
allPs)
, roRange :: Range
roRange = Range
emptyRange
, roVars :: Map Name Schema
roVars = Map Name Schema -> Map Name Schema -> Map Name Schema
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union
((ModVParam -> Schema) -> Map Name ModVParam -> Map Name Schema
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ModVParam -> Schema
mvpType (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
allPs))
(InferInput -> Map Name Schema
inpVars InferInput
env)
}
rw :: RW
rw = RW { woProofObligations :: [Schema]
woProofObligations = [] }
data Error =
TypeMismatch String Schema Schema
| ExpectedMono Schema
| TupleSelectorOutOfRange Int Int
| MissingField Ident [Ident]
| UnexpectedTupleShape Int Int
| UnexpectedRecordShape [Ident] [Ident]
| UnexpectedSequenceShape Int Type
| BadSelector Selector Type
| BadInstantiation
| Captured TVar
| BadProofNoAbs
| BadProofTyVars [TParam]
| KindMismatch Kind Kind
| NotEnoughArgumentsInKind Kind
| BadApplication Type Type
| FreeTypeVariable TVar
| BadTypeApplication Kind [Kind]
| RepeatedVariableInForall TParam
| BadMatch Type
| EmptyArm
| UndefinedTypeVaraible TVar
| UndefinedVariable Name
deriving Int -> Error -> String -> String
[Error] -> String -> String
Error -> String
(Int -> Error -> String -> String)
-> (Error -> String) -> ([Error] -> String -> String) -> Show Error
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Error -> String -> String
showsPrec :: Int -> Error -> String -> String
$cshow :: Error -> String
show :: Error -> String
$cshowList :: [Error] -> String -> String
showList :: [Error] -> String -> String
Show
reportError :: Error -> TcM a
reportError :: forall a. Error -> TcM a
reportError Error
e = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a b. (a -> b) -> a -> b
$
do RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
(Range, Error)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall a.
(Range, Error)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall (m :: * -> *) i a. ExceptionM m i => i -> m a
raise (RO -> Range
roRange RO
ro, Error
e)
withTVar :: TParam -> TcM a -> TcM a
withTVar :: forall a. TParam -> TcM a -> TcM a
withTVar TParam
a (TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m) = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a b. (a -> b) -> a -> b
$
do RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall a.
RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
local RO
ro { roTVars :: Map Int TParam
roTVars = Int -> TParam -> Map Int TParam -> Map Int TParam
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (TParam -> Int
tpUnique TParam
a) TParam
a (RO -> Map Int TParam
roTVars RO
ro) } ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m
withRange :: Range -> TcM a -> TcM a
withRange :: forall a. Range -> TcM a -> TcM a
withRange Range
rng (TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m) = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a b. (a -> b) -> a -> b
$
do RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall a.
RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
local RO
ro { roRange :: Range
roRange = Range
rng } ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m
withAsmp :: Prop -> TcM a -> TcM a
withAsmp :: forall a. Type -> TcM a -> TcM a
withAsmp Type
p (TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m) = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a b. (a -> b) -> a -> b
$
do RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall a.
RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
local RO
ro { roAsmps :: [Type]
roAsmps = Type
p Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: RO -> [Type]
roAsmps RO
ro } ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m
withVar :: Name -> Type -> TcM a -> TcM a
withVar :: forall a. Name -> Type -> TcM a -> TcM a
withVar Name
x Type
t = [(Name, Schema)] -> TcM a -> TcM a
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars [(Name
x,Type -> Schema
tMono Type
t)]
withVars :: [(Name, Schema)] -> TcM a -> TcM a
withVars :: forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars [(Name, Schema)]
xs (TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m) = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
forall a b. (a -> b) -> a -> b
$
do RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall a.
RO
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
local RO
ro { roVars :: Map Name Schema
roVars = Map Name Schema -> Map Name Schema -> Map Name Schema
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ([(Name, Schema)] -> Map Name Schema
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Name, Schema)]
xs) (RO -> Map Name Schema
roVars RO
ro) } ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
m
proofObligation :: Prop -> TcM ()
proofObligation :: Type -> TcM ()
proofObligation Type
p = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) () -> TcM ()
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) ()
-> TcM ())
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) ()
-> TcM ()
forall a b. (a -> b) -> a -> b
$
do RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
(RW -> RW)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) ()
forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ ((RW -> RW)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) ())
-> (RW -> RW)
-> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) ()
forall a b. (a -> b) -> a -> b
$ \RW
rw -> RW
rw { woProofObligations :: [Schema]
woProofObligations =
[TParam] -> [Type] -> Type -> Schema
Forall (Map Int TParam -> [TParam]
forall k a. Map k a -> [a]
Map.elems (RO -> Map Int TParam
roTVars RO
ro)) (RO -> [Type]
roAsmps RO
ro) Type
p
Schema -> [Schema] -> [Schema]
forall a. a -> [a] -> [a]
: RW -> [Schema]
woProofObligations RW
rw }
lookupTVar :: TVar -> TcM Kind
lookupTVar :: TVar -> TcM Kind
lookupTVar TVar
x =
case TVar
x of
TVFree {} -> Error -> TcM Kind
forall a. Error -> TcM a
reportError (TVar -> Error
FreeTypeVariable TVar
x)
TVBound TParam
tpv ->
do let u :: Int
u = TParam -> Int
tpUnique TParam
tpv
k :: Kind
k = TParam -> Kind
tpKind TParam
tpv
RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO -> TcM RO
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
case Int -> Map Int TParam -> Maybe TParam
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
u (RO -> Map Int TParam
roTVars RO
ro) of
Just TParam
tp
| TParam -> Kind
forall t. HasKind t => t -> Kind
kindOf TParam
tp Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k -> Kind -> TcM Kind
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
| Bool
otherwise -> Error -> TcM Kind
forall a. Error -> TcM a
reportError (Error -> TcM Kind) -> Error -> TcM Kind
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> Error
KindMismatch (TParam -> Kind
forall t. HasKind t => t -> Kind
kindOf TParam
tp) Kind
k
Maybe TParam
Nothing -> Error -> TcM Kind
forall a. Error -> TcM a
reportError (Error -> TcM Kind) -> Error -> TcM Kind
forall a b. (a -> b) -> a -> b
$ TVar -> Error
UndefinedTypeVaraible TVar
x
lookupVar :: Name -> TcM Schema
lookupVar :: Name -> TcM Schema
lookupVar Name
x =
do RO
ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO -> TcM RO
forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
case Name -> Map Name Schema -> Maybe Schema
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (RO -> Map Name Schema
roVars RO
ro) of
Just Schema
s -> Schema -> TcM Schema
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return Schema
s
Maybe Schema
Nothing -> Error -> TcM Schema
forall a. Error -> TcM a
reportError (Error -> TcM Schema) -> Error -> TcM Schema
forall a b. (a -> b) -> a -> b
$ Name -> Error
UndefinedVariable Name
x
instance PP Error where
ppPrec :: Int -> Error -> Doc
ppPrec Int
_ Error
err =
case Error
err of
TypeMismatch String
what Schema
expected Schema
actual ->
Doc -> [Doc] -> Doc
ppErr (Doc
"Type mismatch in" Doc -> Doc -> Doc
<+> String -> Doc
text String
what)
[ Doc
"Expected:" Doc -> Doc -> Doc
<+> Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
expected
, Doc
"Actual :" Doc -> Doc -> Doc
<+> Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
actual
]
ExpectedMono Schema
s ->
Doc -> [Doc] -> Doc
ppErr Doc
"Not a monomorphic type"
[ Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
s ]
TupleSelectorOutOfRange Int
sel Int
sz ->
Doc -> [Doc] -> Doc
ppErr Doc
"Tuple selector out of range"
[ Doc
"Selector:" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
sel
, Doc
"Size :" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
sz
]
MissingField Ident
f [Ident]
fs ->
Doc -> [Doc] -> Doc
ppErr Doc
"Invalid record selector"
[ Doc
"Field: " Doc -> Doc -> Doc
<+> Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
f
, Doc
"Fields:" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep ((Ident -> Doc) -> [Ident] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Ident -> Doc
forall a. PP a => a -> Doc
pp [Ident]
fs)
]
UnexpectedTupleShape Int
expected Int
actual ->
Doc -> [Doc] -> Doc
ppErr Doc
"Unexpected tuple shape"
[ Doc
"Expected:" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
expected
, Doc
"Actual :" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
actual
]
UnexpectedRecordShape [Ident]
expected [Ident]
actual ->
Doc -> [Doc] -> Doc
ppErr Doc
"Unexpected record shape"
[ Doc
"Expected:" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep ((Ident -> Doc) -> [Ident] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Ident -> Doc
forall a. PP a => a -> Doc
pp [Ident]
expected)
, Doc
"Actual :" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep ((Ident -> Doc) -> [Ident] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Ident -> Doc
forall a. PP a => a -> Doc
pp [Ident]
actual)
]
UnexpectedSequenceShape Int
n Type
t ->
Doc -> [Doc] -> Doc
ppErr Doc
"Unexpected sequence shape"
[ Doc
"Expected:" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
n
, Doc
"Actual :" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
t
]
BadSelector Selector
sel Type
t ->
Doc -> [Doc] -> Doc
ppErr Doc
"Bad selector"
[ Doc
"Selector:" Doc -> Doc -> Doc
<+> Selector -> Doc
forall a. PP a => a -> Doc
pp Selector
sel
, Doc
"Type :" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
t
]
Error
BadInstantiation ->
Doc -> [Doc] -> Doc
ppErr Doc
"Bad instantiation" []
Captured TVar
x ->
Doc -> [Doc] -> Doc
ppErr Doc
"Captured type variable"
[ Doc
"Variable:" Doc -> Doc -> Doc
<+> TVar -> Doc
forall a. PP a => a -> Doc
pp TVar
x ]
Error
BadProofNoAbs ->
Doc -> [Doc] -> Doc
ppErr Doc
"Proof application without a proof abstraction" []
BadProofTyVars [TParam]
xs ->
Doc -> [Doc] -> Doc
ppErr Doc
"Proof application with type abstraction"
[ Doc
"Type parameter:" Doc -> Doc -> Doc
<+> TParam -> Doc
forall a. PP a => a -> Doc
pp TParam
x | TParam
x <- [TParam]
xs ]
KindMismatch Kind
expected Kind
actual ->
Doc -> [Doc] -> Doc
ppErr Doc
"Kind mismatch"
[ Doc
"Expected:" Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. PP a => a -> Doc
pp Kind
expected
, Doc
"Actual :" Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. PP a => a -> Doc
pp Kind
actual
]
NotEnoughArgumentsInKind Kind
k ->
Doc -> [Doc] -> Doc
ppErr Doc
"Not enough arguments in kind" [ Kind -> Doc
forall a. PP a => a -> Doc
pp Kind
k ]
BadApplication Type
t1 Type
t2 ->
Doc -> [Doc] -> Doc
ppErr Doc
"Bad application"
[ Doc
"Function:" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
t1
, Doc
"Argument:" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
t2
]
FreeTypeVariable TVar
x ->
Doc -> [Doc] -> Doc
ppErr Doc
"Free type variable"
[ Doc
"Variable:" Doc -> Doc -> Doc
<+> TVar -> Doc
forall a. PP a => a -> Doc
pp TVar
x ]
BadTypeApplication Kind
kf [Kind]
ka ->
Doc -> [Doc] -> Doc
ppErr Doc
"Bad type application"
[ Doc
"Function :" Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. PP a => a -> Doc
pp Kind
kf
, Doc
"Arguments:" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep ((Kind -> Doc) -> [Kind] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Kind -> Doc
forall a. PP a => a -> Doc
pp [Kind]
ka)
]
RepeatedVariableInForall TParam
x ->
Doc -> [Doc] -> Doc
ppErr Doc
"Repeated variable in forall"
[ Doc
"Variable:" Doc -> Doc -> Doc
<+> TParam -> Doc
forall a. PP a => a -> Doc
pp TParam
x ]
BadMatch Type
t ->
Doc -> [Doc] -> Doc
ppErr Doc
"Bad match"
[ Doc
"Type:" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
t ]
Error
EmptyArm -> Doc -> [Doc] -> Doc
ppErr Doc
"Empty comprehension arm" []
UndefinedTypeVaraible TVar
x ->
Doc -> [Doc] -> Doc
ppErr Doc
"Undefined type variable"
[ Doc
"Variable:" Doc -> Doc -> Doc
<+> TVar -> Doc
forall a. PP a => a -> Doc
pp TVar
x ]
UndefinedVariable Name
x ->
Doc -> [Doc] -> Doc
ppErr Doc
"Undefined variable"
[ Doc
"Variable:" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp Name
x ]
where
ppErr :: Doc -> [Doc] -> Doc
ppErr Doc
x [Doc]
ys = Doc -> Int -> Doc -> Doc
hang Doc
x Int
2 ([Doc] -> Doc
vcat [ Doc
"•" Doc -> Doc -> Doc
<+> Doc
y | Doc
y <- [Doc]
ys ])