{-# 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 = 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 forall a.
InferInput -> TcM a -> Either (Range, Error) (a, [Schema])
runTcM InferInput
env ([DeclGroup] -> TcM ()
checkDecls [DeclGroup]
ds0) of
Left (Range, Error)
err -> forall a b. a -> Either a b
Left (Range, Error)
err
Right (()
_,[Schema]
ps) -> 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 forall a.
InferInput -> TcM a -> Either (Range, Error) (a, [Schema])
runTcM InferInput
env TcM ()
check of
Left (Range, Error)
err -> forall a b. a -> Either a b
Left (Range, Error)
err
Right (()
_,[Schema]
ps) -> forall a b. b -> Either a b
Right [Schema]
ps
where check :: TcM ()
check = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. TParam -> TcM a -> TcM a
withTVar TcM ()
k1 (forall a b. (a -> b) -> [a] -> [b]
map ModTParam -> TParam
mtpParam (forall k a. Map k a -> [a]
Map.elems (forall mname. ModuleG mname -> Map Name ModTParam
mParamTypes Module
m)))
k1 :: TcM ()
k1 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Type -> TcM a -> TcM a
withAsmp TcM ()
k2 (forall a b. (a -> b) -> [a] -> [b]
map forall a. Located a -> a
thing (forall mname. ModuleG mname -> [Located Type]
mParamConstraints Module
m))
k2 :: TcM ()
k2 = forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars (forall k a. Map k a -> [(k, a)]
Map.toList (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ModVParam -> Schema
mvpType (forall mname. ModuleG mname -> Map Name ModVParam
mParamFuns Module
m)))
forall a b. (a -> b) -> a -> b
$ [DeclGroup] -> TcM ()
checkDecls (forall mname. ModuleG mname -> [DeclGroup]
mDecls Module
m)
onlyNonTrivial :: [ProofObligation] -> [ProofObligation]
onlyNonTrivial :: [Schema] -> [Schema]
onlyNonTrivial = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not 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 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 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
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
DeclGroup
d : [DeclGroup]
ds -> do [(Name, Schema)]
xs <- DeclGroup -> TcM [(Name, Schema)]
checkDeclGroup DeclGroup
d
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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> TcM Kind
checkType [Type]
ts
Kind -> [Kind] -> TcM Kind
checkKind (forall t. HasKind t => t -> Kind
kindOf TCon
tc) [Kind]
ks
TNewtype Newtype
nt [Type]
ts ->
do [Kind]
ks <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> TcM Kind
checkType [Type]
ts
Kind -> [Kind] -> TcM Kind
checkKind (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 forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ RecordMap Ident Type
fs forall a b. (a -> b) -> a -> b
$ \Type
t ->
do Kind
k <- Type -> TcM Kind
checkType Type
t
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Kind
k forall a. Eq a => a -> a -> Bool
== Kind
KType) forall a b. (a -> b) -> a -> b
$ forall a. Error -> TcM a
reportError forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> Error
KindMismatch Kind
KType Kind
k
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
_ -> forall a. Error -> TcM a
reportError forall a b. (a -> b) -> a -> b
$ Kind -> Error
NotEnoughArgumentsInKind Kind
k
Kind
KProp -> forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
Kind
KNum -> forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
Kind
KType -> forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
checkKind (Kind
k1 :-> Kind
k2) (Kind
k : [Kind]
ks)
| Kind
k forall a. Eq a => a -> a -> Bool
== Kind
k1 = Kind -> [Kind] -> TcM Kind
checkKind Kind
k2 [Kind]
ks
| Bool
otherwise = forall a. Error -> TcM a
reportError forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> Error
KindMismatch Kind
k1 Kind
k
checkKind Kind
k [Kind]
ks = forall a. Error -> TcM a
reportError 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
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Kind
k forall a. Eq a => a -> a -> Bool
== Kind
k1) forall a b. (a -> b) -> a -> b
$ forall a. Error -> TcM a
reportError 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) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. TParam -> TcM a -> TcM a
withTVar TcM ()
check [TParam]
as
where check :: TcM ()
check = do 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 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 forall a. Same a => a -> a -> AreSame
same Schema
x Schema
y of
AreSame
NotSame -> forall a. Error -> TcM a
reportError (String -> Schema -> Schema -> Error
TypeMismatch String
msg Schema
x Schema
y)
SameIf [Type]
ps -> 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) = forall a. Same a => a -> a -> AreSame
same a
x a
y AreSame -> AreSame -> AreSame
`sameAnd` 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 forall a. Eq a => a -> a -> Bool
== a
y) AreSame -> AreSame -> AreSame
`sameAnd` 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 forall a. Eq a => a -> a -> Bool
/= Kind
k2 = AreSame
NotSame
| Kind
k1 forall a. Eq a => a -> a -> Bool
== Kind
KNum = if Type
t1 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 forall a. Eq a => a -> a -> Bool
== TVar
y)
(TRec RecordMap Ident Type
x, TRec RecordMap Ident Type
y) -> forall a. Same a => a -> a -> AreSame
same (forall {a} {b}. RecordMap a b -> [Field a b]
mkRec RecordMap Ident Type
x) (forall {a} {b}. RecordMap a b -> [Field a b]
mkRec RecordMap Ident Type
y)
(TNewtype Newtype
x [Type]
xs, TNewtype Newtype
y [Type]
ys) -> forall a. Same a => a -> a -> AreSame
same (forall a b. a -> b -> Field a b
Field Newtype
x [Type]
xs) (forall a b. a -> b -> Field a b
Field Newtype
y [Type]
ys)
(TCon TCon
x [Type]
xs, TCon TCon
y [Type]
ys) -> forall a. Same a => a -> a -> AreSame
same (forall a b. a -> b -> Field a b
Field TCon
x [Type]
xs) (forall a b. a -> b -> Field a b
Field TCon
y [Type]
ys)
(Type, Type)
_ -> AreSame
NotSame
where
k1 :: Kind
k1 = forall t. HasKind t => t -> Kind
kindOf Type
t1
k2 :: Kind
k2 = forall t. HasKind t => t -> Kind
kindOf Type
t2
mkRec :: RecordMap a b -> [Field a b]
mkRec RecordMap a b
r = [ forall a b. a -> b -> Field a b
Field a
x b
y | (a
x,b
y) <- 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) =
forall a. Same a => a -> a -> AreSame
same [TParam]
xs [TParam]
ys AreSame -> AreSame -> AreSame
`sameAnd` forall a. Same a => a -> a -> AreSame
same [Type]
ps [Type]
qs AreSame -> AreSame -> AreSame
`sameAnd` 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 forall a. Eq a => a -> a -> Bool
== TParam -> Maybe Name
tpName TParam
y Bool -> Bool -> Bool
&& TParam -> Kind
tpKind TParam
x 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
Maybe Type
Nothing -> 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 -> 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
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Expr]
es 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
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Schema
tMono forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
tSeq (forall a. Integral a => a -> Type
tNum (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es)) Type
t
ETuple [Expr]
es ->
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type -> Schema
tMono forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type] -> Type
tTuple) (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Expr -> TcM Type
exprType [Expr]
es)
ERec RecordMap Ident Expr
fs ->
do RecordMap Ident Type
fs1 <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr -> TcM Type
exprType RecordMap Ident Expr
fs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Schema
tMono 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
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
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
forall (m :: * -> *) a. Monad m => a -> m a
return 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) <- forall a b. [(a, b)] -> ([a], [b])
unzip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM [Match] -> TcM ([(Name, Schema)], Type)
checkArm [[Match]]
mss
Type
elT <- forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Name, Schema)]]
xs) forall a b. (a -> b) -> a -> b
$ Expr -> TcM Type
exprType Expr
e
case [Type]
ls of
[] -> 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 (forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
tMin [Type]
ls) Type
elT)
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 <- forall a. TParam -> TcM a -> TcM a
withTVar TParam
a (Expr -> TcM Schema
exprSchema Expr
e)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Eq a => a -> a -> Bool
== TParam
a) [TParam]
as) forall a b. (a -> b) -> a -> b
$
forall a. Error -> TcM a
reportError forall a b. (a -> b) -> a -> b
$ TParam -> Error
RepeatedVariableInForall TParam
a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TParam] -> [Type] -> Type -> Schema
Forall (TParam
a 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 = forall t. FVS t => t -> Set TVar
fvs Type
t
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar [TParam]
as) forall a b. (a -> b) -> a -> b
$ \TVar
b ->
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TVar
b forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
vs) forall a b. (a -> b) -> a -> b
$ forall a. Error -> TcM a
reportError forall a b. (a -> b) -> a -> b
$ TVar -> Error
Captured TVar
b
let k' :: Kind
k' = forall t. HasKind t => t -> Kind
kindOf TParam
a
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Kind
k forall a. Eq a => a -> a -> Bool
== Kind
k') forall a b. (a -> b) -> a -> b
$ forall a. Error -> TcM a
reportError 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
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [TParam] -> [Type] -> Type -> Schema
Forall [TParam]
as (forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Type]
ps) (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t1)
Forall [] [Type]
_ Type
_ -> 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 <- forall a. Same a => a -> a -> AreSame
same Type
a Type
t2 ->
do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> TcM ()
proofObligation [Type]
ps
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Schema
tMono Type
b)
Type
tf -> 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 <- forall a. Name -> Type -> TcM a -> TcM a
withVar Name
x Type
t (Expr -> TcM Type
exprType Expr
e)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Schema
tMono 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
forall a. Type -> TcM a -> TcM a
withAsmp Type
p forall a b. (a -> b) -> a -> b
$ do Forall [TParam]
as [Type]
ps Type
t <- Expr -> TcM Schema
exprSchema Expr
e
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [TParam] -> [Type] -> Type -> Schema
Forall [TParam]
as (Type
p 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
forall (m :: * -> *) a. Monad m => a -> m a
return ([TParam] -> [Type] -> Type -> Schema
Forall [] [Type]
qs Type
t)
([], [Type]
_) -> forall a. Error -> TcM a
reportError Error
BadProofNoAbs
([TParam]
_,[Type]
_) -> 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
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 ->
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 ->
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
sz forall a. Eq a => a -> a -> Bool
/= Int
sz1) (forall a. Error -> TcM a
reportError (Int -> Int -> Error
UnexpectedTupleShape Int
sz1 Int
sz))
Maybe Int
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n forall a. Ord a => a -> a -> Bool
< Int
sz) forall a b. (a -> b) -> a -> b
$ forall a. Error -> TcM a
reportError (Int -> Int -> Error
TupleSelectorOutOfRange Int
n Int
sz)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Type]
ts forall a. [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
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
forall (m :: * -> *) a. Monad m => a -> m a
return (TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCFun) [Type
a,Type
res])
Type
_ -> forall a. Error -> TcM a
reportError 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just [Ident]
fs1 ->
do let ns :: [Ident]
ns = forall a. Set a -> [a]
Set.toList (forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Type
fs)
ns1 :: [Ident]
ns1 = forall a. Ord a => [a] -> [a]
sort [Ident]
fs1
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Ident]
ns forall a. Eq a => a -> a -> Bool
== [Ident]
ns1) forall a b. (a -> b) -> a -> b
$
forall a. Error -> TcM a
reportError forall a b. (a -> b) -> a -> b
$ [Ident] -> [Ident] -> Error
UnexpectedRecordShape [Ident]
ns1 [Ident]
ns
case forall a b. Ord a => a -> RecordMap a b -> Maybe b
lookupField Ident
f RecordMap Ident Type
fs of
Maybe Type
Nothing -> forall a. Error -> TcM a
reportError forall a b. (a -> b) -> a -> b
$ Ident -> [Ident] -> Error
MissingField Ident
f forall a b. (a -> b) -> a -> b
$ forall a b. RecordMap a b -> [a]
displayOrder RecordMap Ident Type
fs
Just Type
ft -> 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
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
forall (m :: * -> *) a. Monad m => a -> m a
return (TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCFun) [Type
a,Type
res])
Type
_ -> forall a. Error -> TcM a
reportError 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 -> 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 forall a. Eq a => a -> a -> Bool
== forall a. Integral a => a -> Integer
toInteger Int
len -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Type
_ -> forall a. Error -> TcM a
reportError forall a b. (a -> b) -> a -> b
$ Int -> Type -> Error
UnexpectedSequenceShape Int
len Type
n
forall (m :: * -> *) a. Monad m => a -> m a
return Type
elT
Type
_ -> forall a. Error -> TcM a
reportError 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 forall a. Eq a => a -> a -> Bool
/= Kind
k2 = forall a. Error -> TcM a
reportError (Kind -> Kind -> Error
KindMismatch Kind
k1 Kind
k2)
| Kind
k1 forall a. Eq a => a -> a -> Bool
== Kind
KNum = Type -> TcM ()
proofObligation (Type
t1 Type -> Type -> Type
=#= Type
t2)
where
k1 :: Kind
k1 = forall t. HasKind t => t -> Kind
kindOf Type
t1
k2 :: Kind
k2 = 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 = forall a. Error -> TcM a
reportError 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 [] [] = 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 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Type] -> [Type] -> TcM ()
goMany [Type]
xs [Type]
ys
goMany [Type]
_ [Type]
_ = 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 forall a. Eq a => a -> a -> Bool
== TVar
y -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Type
_ -> forall {a}. TcM a
err
TCon TCon
tc1 [Type]
ts1 -> case Type
other of
TCon TCon
tc2 [Type]
ts2
| TCon
tc1 forall a. Eq a => a -> a -> Bool
== TCon
tc2 -> [Type] -> [Type] -> TcM ()
goMany [Type]
ts1 [Type]
ts2
Type
_ -> forall {a}. TcM a
err
TNewtype Newtype
nt1 [Type]
ts1 ->
case Type
other of
TNewtype Newtype
nt2 [Type]
ts2
| Newtype
nt1 forall a. Eq a => a -> a -> Bool
== Newtype
nt2 -> [Type] -> [Type] -> TcM ()
goMany [Type]
ts1 [Type]
ts2
Type
_ -> forall {a}. TcM a
err
TRec RecordMap Ident Type
fs ->
case Type
other of
TRec RecordMap Ident Type
gs ->
do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Type
fs forall a. Eq a => a -> a -> Bool
== forall a b. Ord a => RecordMap a b -> Set a
fieldSet RecordMap Ident Type
gs) forall {a}. TcM a
err
[Type] -> [Type] -> TcM ()
goMany (forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs) (forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
gs)
Type
_ -> 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 forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkSig forall a b. (a -> b) -> a -> b
$ Schema -> TcM ()
checkSchema forall a b. (a -> b) -> a -> b
$ Decl -> Schema
dSignature Decl
d
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Name
dName Decl
d, Decl -> Schema
dSignature Decl
d)
DForeign FFIFunType
_ ->
do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkSig forall a b. (a -> b) -> a -> b
$ Schema -> TcM ()
checkSchema forall a b. (a -> b) -> a -> b
$ Decl -> Schema
dSignature Decl
d
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
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkSig 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 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. PP a => a -> Doc
pp Name
nm) forall a. [a] -> [a] -> [a]
++
String
", at " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. PP a => a -> Doc
pp (Name -> Range
nameLoc Name
nm))
String -> Schema -> Schema -> TcM ()
sameSchemas String
loc Schema
s Schema
s1
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
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, Schema)
x]
Recursive [Decl]
ds ->
do [(Name, Schema)]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Decl]
ds forall a b. (a -> b) -> a -> b
$ \Decl
d ->
do Schema -> TcM ()
checkSchema (Decl -> Schema
dSignature Decl
d)
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Name
dName Decl
d, Decl -> Schema
dSignature Decl
d)
forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars [(Name, Schema)]
xs forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t 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 <- forall a. Same a => a -> a -> AreSame
same Type
elt Type
el ->
do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> TcM ()
proofObligation [Type]
ps
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
x, Type -> Schema
tMono Type
elt), Type
l)
| Bool
otherwise -> forall a. Error -> TcM a
reportError 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
_ -> forall a. Error -> TcM a
reportError 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
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name, Schema)
x, forall a. Integral a => a -> Type
tNum (Int
1 :: Int))
checkArm :: [Match] -> TcM ([(Name, Schema)], Type)
checkArm :: [Match] -> TcM ([(Name, Schema)], Type)
checkArm [] = 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
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) <- forall a. [(Name, Schema)] -> TcM a -> TcM a
withVars [(Name, Schema)
x] 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
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if forall a b. (a, b) -> a
fst (Name, Schema)
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Schema)]
xs
then ([(Name, Schema)]
xs, Type
newLen)
else ((Name, Schema)
x 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 = 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 = forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a)
<*> :: forall a 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 = 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 = 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 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
_) -> forall a b. a -> Either a b
Left (Range, Error)
err
(Right a
a, RW
s) -> 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 = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (TParam -> Int
tpUnique TParam
x, TParam
x)
| ModTParam
tp <- 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 = forall a b. (a -> b) -> [a] -> [b]
map forall a. Located a -> a
thing (ModParamNames -> [Located Type]
mpnConstraints ModParamNames
allPs)
, roRange :: Range
roRange = Range
emptyRange
, roVars :: Map Name Schema
roVars = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union
(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 -> ShowS
[Error] -> ShowS
Error -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Error] -> ShowS
$cshowList :: [Error] -> ShowS
show :: Error -> String
$cshow :: Error -> String
showsPrec :: Int -> Error -> ShowS
$cshowsPrec :: Int -> Error -> ShowS
Show
reportError :: Error -> TcM a
reportError :: forall a. Error -> TcM a
reportError Error
e = forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM forall a b. (a -> b) -> a -> b
$
do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
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) = forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM forall a b. (a -> b) -> a -> b
$
do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
local RO
ro { roTVars :: Map Int TParam
roTVars = 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) = forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM forall a b. (a -> b) -> a -> b
$
do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
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) = forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM forall a b. (a -> b) -> a -> b
$
do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
local RO
ro { roAsmps :: [Type]
roAsmps = Type
p 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 = 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) = forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM forall a b. (a -> b) -> a -> b
$
do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
local RO
ro { roVars :: Map Name Schema
roVars = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (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 = forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM forall a b. (a -> b) -> a -> b
$
do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
sets_ forall a b. (a -> b) -> a -> b
$ \RW
rw -> RW
rw { woProofObligations :: [Schema]
woProofObligations =
[TParam] -> [Type] -> Type -> Schema
Forall (forall k a. Map k a -> [a]
Map.elems (RO -> Map Int TParam
roTVars RO
ro)) (RO -> [Type]
roAsmps RO
ro) Type
p
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 {} -> 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 <- forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM forall (m :: * -> *) i. ReaderM m i => m i
ask
case 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
| forall t. HasKind t => t -> Kind
kindOf TParam
tp forall a. Eq a => a -> a -> Bool
== Kind
k -> forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
| Bool
otherwise -> forall a. Error -> TcM a
reportError forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> Error
KindMismatch (forall t. HasKind t => t -> Kind
kindOf TParam
tp) Kind
k
Maybe TParam
Nothing -> forall a. Error -> TcM a
reportError 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 <- forall a.
ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
TcM forall (m :: * -> *) i. ReaderM m i => m i
ask
case 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Schema
s
Maybe Schema
Nothing -> forall a. Error -> TcM a
reportError 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
<+> forall a. PP a => a -> Doc
pp Schema
expected
, Doc
"Actual :" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Schema
actual
]
ExpectedMono Schema
s ->
Doc -> [Doc] -> Doc
ppErr Doc
"Not a monomorphic type"
[ 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
<+> forall a. PP a => a -> Doc
pp Ident
f
, Doc
"Fields:" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep (forall a b. (a -> b) -> [a] -> [b]
map 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 (forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => a -> Doc
pp [Ident]
expected)
, Doc
"Actual :" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep (forall a b. (a -> b) -> [a] -> [b]
map 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
<+> 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
<+> forall a. PP a => a -> Doc
pp Selector
sel
, Doc
"Type :" Doc -> Doc -> 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
<+> 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
<+> 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
<+> forall a. PP a => a -> Doc
pp Kind
expected
, Doc
"Actual :" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Kind
actual
]
NotEnoughArgumentsInKind Kind
k ->
Doc -> [Doc] -> Doc
ppErr Doc
"Not enough arguments in kind" [ 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
<+> forall a. PP a => a -> Doc
pp Type
t1
, Doc
"Argument:" Doc -> Doc -> 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
<+> 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
<+> forall a. PP a => a -> Doc
pp Kind
kf
, Doc
"Arguments:" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep (forall a b. (a -> b) -> [a] -> [b]
map 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
<+> forall a. PP a => a -> Doc
pp TParam
x ]
BadMatch Type
t ->
Doc -> [Doc] -> Doc
ppErr Doc
"Bad match"
[ Doc
"Type:" Doc -> Doc -> 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
<+> forall a. PP a => a -> Doc
pp TVar
x ]
UndefinedVariable Name
x ->
Doc -> [Doc] -> Doc
ppErr Doc
"Undefined variable"
[ Doc
"Variable:" Doc -> Doc -> 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 ])