{-# Language OverloadedStrings #-}
module Cryptol.TypeCheck.Instantiate
( instantiateWith
, TypeArg(..)
, uncheckedTypeArg
, MaybeCheckedType(..)
) where
import Cryptol.ModuleSystem.Name (nameIdent)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Monad
import Cryptol.TypeCheck.Subst (listParamSubst, apSubst)
import Cryptol.TypeCheck.Kind(checkType)
import Cryptol.TypeCheck.Error
import Cryptol.Parser.Position (Located(..))
import Cryptol.Utils.Ident (Ident)
import Cryptol.Utils.Panic(panic)
import qualified Cryptol.Parser.AST as P
import Control.Monad(zipWithM)
import Data.Function (on)
import Data.List(sortBy, groupBy, find)
import Data.Maybe(mapMaybe,isJust)
import Data.Either(partitionEithers)
import qualified Data.Set as Set
data TypeArg = TypeArg
{ TypeArg -> Maybe (Located Ident)
tyArgName :: Maybe (Located Ident)
, TypeArg -> MaybeCheckedType
tyArgType :: MaybeCheckedType
}
uncheckedTypeArg :: P.TypeInst Name -> TypeArg
uncheckedTypeArg :: TypeInst Name -> TypeArg
uncheckedTypeArg a :: TypeInst Name
a =
case TypeInst Name
a of
P.NamedInst x :: Named (Type Name)
x ->
TypeArg :: Maybe (Located Ident) -> MaybeCheckedType -> TypeArg
TypeArg { tyArgName :: Maybe (Located Ident)
tyArgName = Located Ident -> Maybe (Located Ident)
forall a. a -> Maybe a
Just (Named (Type Name) -> Located Ident
forall a. Named a -> Located Ident
P.name Named (Type Name)
x), tyArgType :: MaybeCheckedType
tyArgType = Type Name -> MaybeCheckedType
Unchecked (Named (Type Name) -> Type Name
forall a. Named a -> a
P.value Named (Type Name)
x) }
P.PosInst t :: Type Name
t ->
TypeArg :: Maybe (Located Ident) -> MaybeCheckedType -> TypeArg
TypeArg { tyArgName :: Maybe (Located Ident)
tyArgName = Maybe (Located Ident)
forall a. Maybe a
Nothing, tyArgType :: MaybeCheckedType
tyArgType = Type Name -> MaybeCheckedType
Unchecked Type Name
t }
data MaybeCheckedType = Checked Type | Unchecked (P.Type Name)
checkTyParam :: TVarSource -> Kind -> MaybeCheckedType -> InferM Type
checkTyParam :: TVarSource -> Kind -> MaybeCheckedType -> InferM Type
checkTyParam src :: TVarSource
src k :: Kind
k mb :: MaybeCheckedType
mb =
case MaybeCheckedType
mb of
Checked t :: Type
t
| Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k' -> Type -> InferM Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
| Bool
otherwise -> do Error -> InferM ()
recordError (Kind -> Kind -> Error
KindMismatch Kind
k Kind
k')
TVarSource -> Kind -> InferM Type
newType TVarSource
src Kind
k
where k' :: Kind
k' = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t
Unchecked t :: Type Name
t -> Type Name -> Maybe Kind -> InferM Type
checkType Type Name
t (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
k)
instantiateWith :: Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr,Type)
instantiateWith :: Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Type)
instantiateWith nm :: Name
nm e :: Expr
e s :: Schema
s ts :: [TypeArg]
ts
| [Located (Ident, MaybeCheckedType)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Located (Ident, MaybeCheckedType)]
named = Name -> Expr -> Schema -> [MaybeCheckedType] -> InferM (Expr, Type)
instantiateWithPos Name
nm Expr
e Schema
s [MaybeCheckedType]
positional
| [MaybeCheckedType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [MaybeCheckedType]
positional = Name
-> Expr
-> Schema
-> [Located (Ident, MaybeCheckedType)]
-> InferM (Expr, Type)
instantiateWithNames Name
nm Expr
e Schema
s [Located (Ident, MaybeCheckedType)]
named
| Bool
otherwise = do Error -> InferM ()
recordError Error
CannotMixPositionalAndNamedTypeParams
Name
-> Expr
-> Schema
-> [Located (Ident, MaybeCheckedType)]
-> InferM (Expr, Type)
instantiateWithNames Name
nm Expr
e Schema
s [Located (Ident, MaybeCheckedType)]
named
where
(named :: [Located (Ident, MaybeCheckedType)]
named,positional :: [MaybeCheckedType]
positional) = [Either (Located (Ident, MaybeCheckedType)) MaybeCheckedType]
-> ([Located (Ident, MaybeCheckedType)], [MaybeCheckedType])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ((TypeArg
-> Either (Located (Ident, MaybeCheckedType)) MaybeCheckedType)
-> [TypeArg]
-> [Either (Located (Ident, MaybeCheckedType)) MaybeCheckedType]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg
-> Either (Located (Ident, MaybeCheckedType)) MaybeCheckedType
classify [TypeArg]
ts)
classify :: TypeArg
-> Either (Located (Ident, MaybeCheckedType)) MaybeCheckedType
classify t :: TypeArg
t = case TypeArg -> Maybe (Located Ident)
tyArgName TypeArg
t of
Just n :: Located Ident
n -> Located (Ident, MaybeCheckedType)
-> Either (Located (Ident, MaybeCheckedType)) MaybeCheckedType
forall a b. a -> Either a b
Left Located Ident
n { thing :: (Ident, MaybeCheckedType)
thing = (Located Ident -> Ident
forall a. Located a -> a
thing Located Ident
n, TypeArg -> MaybeCheckedType
tyArgType TypeArg
t) }
Nothing -> MaybeCheckedType
-> Either (Located (Ident, MaybeCheckedType)) MaybeCheckedType
forall a b. b -> Either a b
Right (TypeArg -> MaybeCheckedType
tyArgType TypeArg
t)
instantiateWithPos ::
Name -> Expr -> Schema -> [MaybeCheckedType] -> InferM (Expr,Type)
instantiateWithPos :: Name -> Expr -> Schema -> [MaybeCheckedType] -> InferM (Expr, Type)
instantiateWithPos nm :: Name
nm e :: Expr
e (Forall as :: [TParam]
as ps :: [Type]
ps t :: Type
t) ts :: [MaybeCheckedType]
ts =
do [(TParam, Type)]
su <- Int
-> [(TParam, Type)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Type)]
makeSu (1::Int) [] [TParam]
as [MaybeCheckedType]
ts
[(TParam, Type)] -> Expr -> [Type] -> Type -> InferM (Expr, Type)
doInst [(TParam, Type)]
su Expr
e [Type]
ps Type
t
where
isNamed :: TParam -> Bool
isNamed q :: TParam
q = Maybe Name -> Bool
forall a. Maybe a -> Bool
isJust (TParam -> Maybe Name
tpName TParam
q)
makeSu :: Int
-> [(TParam, Type)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Type)]
makeSu n :: Int
n su :: [(TParam, Type)]
su (q :: TParam
q : qs :: [TParam]
qs) (mbty :: MaybeCheckedType
mbty : tys :: [MaybeCheckedType]
tys)
| Bool -> Bool
not (TParam -> Bool
isNamed TParam
q) = do (TParam, Type)
r <- Int -> TParam -> InferM (TParam, Type)
forall a. HasKind a => Int -> a -> InferM (a, Type)
unnamed Int
n TParam
q
Int
-> [(TParam, Type)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Type)]
makeSu (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) ((TParam, Type)
r (TParam, Type) -> [(TParam, Type)] -> [(TParam, Type)]
forall a. a -> [a] -> [a]
: [(TParam, Type)]
su) [TParam]
qs (MaybeCheckedType
mbty MaybeCheckedType -> [MaybeCheckedType] -> [MaybeCheckedType]
forall a. a -> [a] -> [a]
: [MaybeCheckedType]
tys)
| Bool
otherwise = do Type
ty <- TVarSource -> Kind -> MaybeCheckedType -> InferM Type
checkTyParam (Name -> Int -> TVarSource
TypeParamInstPos Name
nm Int
n) (TParam -> Kind
forall t. HasKind t => t -> Kind
kindOf TParam
q) MaybeCheckedType
mbty
Int
-> [(TParam, Type)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Type)]
makeSu (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) ((TParam
q,Type
ty) (TParam, Type) -> [(TParam, Type)] -> [(TParam, Type)]
forall a. a -> [a] -> [a]
: [(TParam, Type)]
su) [TParam]
qs [MaybeCheckedType]
tys
makeSu _ su :: [(TParam, Type)]
su [] [] = [(TParam, Type)] -> InferM [(TParam, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TParam, Type)] -> [(TParam, Type)]
forall a. [a] -> [a]
reverse [(TParam, Type)]
su)
makeSu n :: Int
n su :: [(TParam, Type)]
su (q :: TParam
q : qs :: [TParam]
qs) [] = do (TParam, Type)
r <- Int -> TParam -> InferM (TParam, Type)
forall a. HasKind a => Int -> a -> InferM (a, Type)
unnamed Int
n TParam
q
Int
-> [(TParam, Type)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Type)]
makeSu (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) ((TParam, Type)
r (TParam, Type) -> [(TParam, Type)] -> [(TParam, Type)]
forall a. a -> [a] -> [a]
: [(TParam, Type)]
su) [TParam]
qs []
makeSu _ su :: [(TParam, Type)]
su [] _ = do Error -> InferM ()
recordError Error
TooManyPositionalTypeParams
[(TParam, Type)] -> InferM [(TParam, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TParam, Type)] -> [(TParam, Type)]
forall a. [a] -> [a]
reverse [(TParam, Type)]
su)
unnamed :: Int -> a -> InferM (a, Type)
unnamed n :: Int
n q :: a
q = do Type
ty <- TVarSource -> Kind -> InferM Type
newType TVarSource
src (a -> Kind
forall t. HasKind t => t -> Kind
kindOf a
q)
(a, Type) -> InferM (a, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
q, Type
ty)
where
src :: TVarSource
src = case Int -> [TParam] -> [TParam]
forall a. Int -> [a] -> [a]
drop (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) [TParam]
as of
p :: TParam
p:_ ->
case TParam -> TPFlavor
tpFlav TParam
p of
TPOther (Just a :: Name
a) -> Name -> Ident -> TVarSource
TypeParamInstNamed Name
nm (Name -> Ident
nameIdent Name
a)
_ -> Name -> Int -> TVarSource
TypeParamInstPos Name
nm Int
n
_ -> String -> [String] -> TVarSource
forall a. HasCallStack => String -> [String] -> a
panic "instantiateWithPos"
[ "Invalid parameter index", Int -> String
forall a. Show a => a -> String
show Int
n, [TParam] -> String
forall a. Show a => a -> String
show [TParam]
as ]
instantiateWithNames ::
Name -> Expr -> Schema -> [Located (Ident,MaybeCheckedType)]
-> InferM (Expr,Type)
instantiateWithNames :: Name
-> Expr
-> Schema
-> [Located (Ident, MaybeCheckedType)]
-> InferM (Expr, Type)
instantiateWithNames nm :: Name
nm e :: Expr
e (Forall as :: [TParam]
as ps :: [Type]
ps t :: Type
t) xs :: [Located (Ident, MaybeCheckedType)]
xs =
do [InferM ()] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [InferM ()]
repeatedParams
(Located (Ident, MaybeCheckedType) -> InferM ())
-> [Located (Ident, MaybeCheckedType)] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Error -> InferM ()
recordError (Error -> InferM ())
-> (Located (Ident, MaybeCheckedType) -> Error)
-> Located (Ident, MaybeCheckedType)
-> InferM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located Ident -> Error
UndefinedTypeParameter (Located Ident -> Error)
-> (Located (Ident, MaybeCheckedType) -> Located Ident)
-> Located (Ident, MaybeCheckedType)
-> Error
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Ident, MaybeCheckedType) -> Ident)
-> Located (Ident, MaybeCheckedType) -> Located Ident
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Ident, MaybeCheckedType) -> Ident
forall a b. (a, b) -> a
fst) [Located (Ident, MaybeCheckedType)]
undefParams
[(TParam, Type)]
su' <- (Int -> TParam -> InferM (TParam, Type))
-> [Int] -> [TParam] -> InferM [(TParam, Type)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Int -> TParam -> InferM (TParam, Type)
paramInst [ 1.. ] [TParam]
as
[(TParam, Type)] -> Expr -> [Type] -> Type -> InferM (Expr, Type)
doInst [(TParam, Type)]
su' Expr
e [Type]
ps Type
t
where
paramInst :: Int -> TParam -> InferM (TParam, Type)
paramInst n :: Int
n x :: TParam
x =
do let k :: Kind
k = TParam -> Kind
tpKind TParam
x
lkp :: Name -> Maybe (Located (Ident, MaybeCheckedType))
lkp name :: Name
name = (Located (Ident, MaybeCheckedType) -> Bool)
-> [Located (Ident, MaybeCheckedType)]
-> Maybe (Located (Ident, MaybeCheckedType))
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\th :: Located (Ident, MaybeCheckedType)
th -> (Ident, MaybeCheckedType) -> Ident
forall a b. (a, b) -> a
fst (Located (Ident, MaybeCheckedType) -> (Ident, MaybeCheckedType)
forall a. Located a -> a
thing Located (Ident, MaybeCheckedType)
th) Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Ident
nameIdent Name
name) [Located (Ident, MaybeCheckedType)]
xs
src :: TVarSource
src = case TParam -> Maybe Name
tpName TParam
x of
Just na :: Name
na -> Name -> Ident -> TVarSource
TypeParamInstNamed Name
nm (Name -> Ident
nameIdent Name
na)
Nothing -> Name -> Int -> TVarSource
TypeParamInstPos Name
nm Int
n
Type
ty <- case Name -> Maybe (Located (Ident, MaybeCheckedType))
lkp (Name -> Maybe (Located (Ident, MaybeCheckedType)))
-> Maybe Name -> Maybe (Located (Ident, MaybeCheckedType))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TParam -> Maybe Name
tpName TParam
x of
Just lty :: Located (Ident, MaybeCheckedType)
lty -> TVarSource -> Kind -> MaybeCheckedType -> InferM Type
checkTyParam TVarSource
src Kind
k ((Ident, MaybeCheckedType) -> MaybeCheckedType
forall a b. (a, b) -> b
snd (Located (Ident, MaybeCheckedType) -> (Ident, MaybeCheckedType)
forall a. Located a -> a
thing Located (Ident, MaybeCheckedType)
lty))
Nothing -> TVarSource -> Kind -> InferM Type
newType TVarSource
src Kind
k
(TParam, Type) -> InferM (TParam, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TParam
x, Type
ty)
repeatedParams :: [InferM ()]
repeatedParams = ([Located (Ident, MaybeCheckedType)] -> Maybe (InferM ()))
-> [[Located (Ident, MaybeCheckedType)]] -> [InferM ()]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe [Located (Ident, MaybeCheckedType)] -> Maybe (InferM ())
forall b. [Located (Ident, b)] -> Maybe (InferM ())
isRepeated
([[Located (Ident, MaybeCheckedType)]] -> [InferM ()])
-> [[Located (Ident, MaybeCheckedType)]] -> [InferM ()]
forall a b. (a -> b) -> a -> b
$ (Located (Ident, MaybeCheckedType)
-> Located (Ident, MaybeCheckedType) -> Bool)
-> [Located (Ident, MaybeCheckedType)]
-> [[Located (Ident, MaybeCheckedType)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Ident -> Ident -> Bool)
-> (Located (Ident, MaybeCheckedType) -> Ident)
-> Located (Ident, MaybeCheckedType)
-> Located (Ident, MaybeCheckedType)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Located (Ident, MaybeCheckedType) -> Ident
forall c b. Located (c, b) -> c
pName)
([Located (Ident, MaybeCheckedType)]
-> [[Located (Ident, MaybeCheckedType)]])
-> [Located (Ident, MaybeCheckedType)]
-> [[Located (Ident, MaybeCheckedType)]]
forall a b. (a -> b) -> a -> b
$ (Located (Ident, MaybeCheckedType)
-> Located (Ident, MaybeCheckedType) -> Ordering)
-> [Located (Ident, MaybeCheckedType)]
-> [Located (Ident, MaybeCheckedType)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Ident -> Ident -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Ident -> Ident -> Ordering)
-> (Located (Ident, MaybeCheckedType) -> Ident)
-> Located (Ident, MaybeCheckedType)
-> Located (Ident, MaybeCheckedType)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Located (Ident, MaybeCheckedType) -> Ident
forall c b. Located (c, b) -> c
pName) [Located (Ident, MaybeCheckedType)]
xs
isRepeated :: [Located (Ident, b)] -> Maybe (InferM ())
isRepeated ys :: [Located (Ident, b)]
ys@(a :: Located (Ident, b)
a : _ : _) =
InferM () -> Maybe (InferM ())
forall a. a -> Maybe a
Just (InferM () -> Maybe (InferM ())) -> InferM () -> Maybe (InferM ())
forall a b. (a -> b) -> a -> b
$ Error -> InferM ()
recordError (Ident -> [Range] -> Error
RepeatedTypeParameter ((Ident, b) -> Ident
forall a b. (a, b) -> a
fst (Located (Ident, b) -> (Ident, b)
forall a. Located a -> a
thing Located (Ident, b)
a)) ((Located (Ident, b) -> Range) -> [Located (Ident, b)] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map Located (Ident, b) -> Range
forall a. Located a -> Range
srcRange [Located (Ident, b)]
ys))
isRepeated _ = Maybe (InferM ())
forall a. Maybe a
Nothing
paramIdents :: [Ident]
paramIdents = [ Name -> Ident
nameIdent Name
n | Just n :: Name
n <- (TParam -> Maybe Name) -> [TParam] -> [Maybe Name]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> Maybe Name
tpName [TParam]
as ]
undefParams :: [Located (Ident, MaybeCheckedType)]
undefParams = [ Located (Ident, MaybeCheckedType)
x | Located (Ident, MaybeCheckedType)
x <- [Located (Ident, MaybeCheckedType)]
xs, Located (Ident, MaybeCheckedType) -> Ident
forall c b. Located (c, b) -> c
pName Located (Ident, MaybeCheckedType)
x Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Ident]
paramIdents ]
pName :: Located (c, b) -> c
pName = (c, b) -> c
forall a b. (a, b) -> a
fst ((c, b) -> c) -> (Located (c, b) -> (c, b)) -> Located (c, b) -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (c, b) -> (c, b)
forall a. Located a -> a
thing
doInst :: [(TParam, Type)] -> Expr -> [Prop] -> Type -> InferM (Expr,Type)
doInst :: [(TParam, Type)] -> Expr -> [Type] -> Type -> InferM (Expr, Type)
doInst su' :: [(TParam, Type)]
su' e :: Expr
e ps :: [Type]
ps t :: Type
t =
do let su :: Subst
su = [(TParam, Type)] -> Subst
listParamSubst [(TParam, Type)]
su'
ConstraintSource -> [Type] -> InferM ()
newGoals (Expr -> ConstraintSource
CtInst Expr
e) ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su) [Type]
ps)
let t1 :: Type
t1 = Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t
[Type]
ps' <- [[Type]] -> [Type]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Type]] -> [Type]) -> InferM [[Type]] -> InferM [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((TParam, Type) -> InferM [Type])
-> [(TParam, Type)] -> InferM [[Type]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TParam, Type) -> InferM [Type]
checkInst [(TParam, Type)]
su'
ConstraintSource -> [Type] -> InferM ()
newGoals (Expr -> ConstraintSource
CtInst Expr
e) [Type]
ps'
(Expr, Type) -> InferM (Expr, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ( Expr -> Expr
addProofParams ([Type] -> Expr -> Expr
forall (t :: * -> *). Foldable t => t Type -> Expr -> Expr
addTyParams (((TParam, Type) -> Type) -> [(TParam, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (TParam, Type) -> Type
forall a b. (a, b) -> b
snd [(TParam, Type)]
su') Expr
e), Type
t1 )
where
addTyParams :: t Type -> Expr -> Expr
addTyParams ts :: t Type
ts e1 :: Expr
e1 = (Expr -> Type -> Expr) -> Expr -> t Type -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Type -> Expr
ETApp Expr
e1 t Type
ts
addProofParams :: Expr -> Expr
addProofParams e1 :: Expr
e1 = (Expr -> Type -> Expr) -> Expr -> [Type] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\e2 :: Expr
e2 _ -> Expr -> Expr
EProofApp Expr
e2) Expr
e1 [Type]
ps
frees :: Set TVar
frees = [Set TVar] -> Set TVar
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((Type -> Set TVar) -> [Type] -> [Set TVar]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (Type
t Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ps))
bounds :: Set TParam
bounds = [Set TParam] -> Set TParam
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((TVar -> Set TParam) -> [TVar] -> [Set TParam]
forall a b. (a -> b) -> [a] -> [b]
map TVar -> Set TParam
scope (Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList Set TVar
frees))
where
scope :: TVar -> Set TParam
scope (TVFree _ _ vs :: Set TParam
vs _) = Set TParam
vs
scope (TVBound _) = Set TParam
forall a. Set a
Set.empty
checkInst :: (TParam, Type) -> InferM [Prop]
checkInst :: (TParam, Type) -> InferM [Type]
checkInst (tp :: TParam
tp, ty :: Type
ty)
| TParam -> Set TParam -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember TParam
tp Set TParam
bounds = [Type] -> InferM [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = Type -> Type -> InferM [Type]
unify (TVar -> Type
TVar (TParam -> TVar
tpVar TParam
tp)) Type
ty