-- |
-- Module      :  Cryptol.TypeCheck.Instantiate
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
{-# 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 TypeInst Name
a =
  case TypeInst Name
a of
    P.NamedInst 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 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 :: TypeSource -> Kind -> MaybeCheckedType -> InferM Type
checkTyParam :: TypeSource -> Kind -> MaybeCheckedType -> InferM Type
checkTyParam TypeSource
src Kind
k MaybeCheckedType
mb =
  case MaybeCheckedType
mb of
    Checked 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 (Maybe TypeSource -> Kind -> Kind -> Error
KindMismatch (TypeSource -> Maybe TypeSource
forall a. a -> Maybe a
Just TypeSource
src) Kind
k Kind
k')
                        TypeSource -> Kind -> InferM Type
newType TypeSource
src Kind
k
        where k' :: Kind
k' = Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t
    Unchecked 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 Name
nm Expr
e Schema
s [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
  ([Located (Ident, MaybeCheckedType)]
named,[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 TypeArg
t = case TypeArg -> Maybe (Located Ident)
tyArgName TypeArg
t of
                 Just 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) }
                 Maybe (Located Ident)
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 Name
nm Expr
e (Forall [TParam]
as [Type]
ps Type
t) [MaybeCheckedType]
ts =
  do [(TParam, Type)]
su <- Int
-> [(TParam, Type)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Type)]
makeSu (Int
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 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 Int
n [(TParam, Type)]
su (TParam
q : [TParam]
qs) (MaybeCheckedType
mbty : [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
+Int
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 <- TypeSource -> Kind -> MaybeCheckedType -> InferM Type
checkTyParam (Name -> Int -> TypeSource
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
+Int
1) ((TParam
q,Type
ty) (TParam, Type) -> [(TParam, Type)] -> [(TParam, Type)]
forall a. a -> [a] -> [a]
: [(TParam, Type)]
su) [TParam]
qs [MaybeCheckedType]
tys

  makeSu Int
_ [(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 Int
n [(TParam, Type)]
su (TParam
q : [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
+Int
1) ((TParam, Type)
r (TParam, Type) -> [(TParam, Type)] -> [(TParam, Type)]
forall a. a -> [a] -> [a]
: [(TParam, Type)]
su) [TParam]
qs []
  makeSu Int
_ [(TParam, Type)]
su [] [MaybeCheckedType]
_        = 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 Int
n a
q = do Type
ty <- TypeSource -> Kind -> InferM Type
newType TypeSource
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 :: TypeSource
src = case Int -> [TParam] -> [TParam]
forall a. Int -> [a] -> [a]
drop (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) {- count from 1 -} [TParam]
as of
            TParam
p:[TParam]
_ ->
              case TParam -> Maybe Name
tpName TParam
p of
                Just Name
a -> Name -> Ident -> TypeSource
TypeParamInstNamed Name
nm (Name -> Ident
nameIdent Name
a)
                Maybe Name
_      -> Name -> Int -> TypeSource
TypeParamInstPos Name
nm Int
n
            [TParam]
_ -> String -> [String] -> TypeSource
forall a. HasCallStack => String -> [String] -> a
panic String
"instantiateWithPos"
                    [ String
"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 ]





{- | Instantiate an expression of the given polymorphic type.
The arguments that are provided will be instantiated as requested,
the rest will be instantiated with fresh type variables.

EProofApp (ETApp e t)

  where
  - There will be one `ETApp t` for each insantiated type parameter;
  - there will be one `EProofApp` for each constraint on the schema;
-}
instantiateWithNames ::
  Name -> Expr -> Schema -> [Located (Ident,MaybeCheckedType)]
                     -> InferM (Expr,Type)
instantiateWithNames :: Name
-> Expr
-> Schema
-> [Located (Ident, MaybeCheckedType)]
-> InferM (Expr, Type)
instantiateWithNames Name
nm Expr
e (Forall [TParam]
as [Type]
ps Type
t) [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 [ Int
1.. ] [TParam]
as
     [(TParam, Type)] -> Expr -> [Type] -> Type -> InferM (Expr, Type)
doInst [(TParam, Type)]
su' Expr
e [Type]
ps Type
t
  where
  -- Choose the type for type parameter `x`
  paramInst :: Int -> TParam -> InferM (TParam, Type)
paramInst Int
n TParam
x =
    do let k :: Kind
k = TParam -> Kind
tpKind TParam
x

           -- We just use nameIdent for comparison here, as all parameter names
           -- should have a NameInfo of Parameter.
           lkp :: Name -> Maybe (Located (Ident, MaybeCheckedType))
lkp 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 (\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 :: TypeSource
src = case TParam -> Maybe Name
tpName TParam
x of
                   Just Name
na -> Name -> Ident -> TypeSource
TypeParamInstNamed Name
nm (Name -> Ident
nameIdent Name
na)
                   Maybe Name
Nothing -> Name -> Int -> TypeSource
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 Located (Ident, MaybeCheckedType)
lty -> TypeSource -> Kind -> MaybeCheckedType -> InferM Type
checkTyParam TypeSource
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))
               Maybe (Located (Ident, MaybeCheckedType))
Nothing -> TypeSource -> Kind -> InferM Type
newType TypeSource
src Kind
k
       (TParam, Type) -> InferM (TParam, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TParam
x, Type
ty)

  -- Errors from multiple values for the same parameter.
  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@(Located (Ident, b)
a : Located (Ident, b)
_ : [Located (Ident, b)]
_)  =
    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 [Located (Ident, b)]
_ = Maybe (InferM ())
forall a. Maybe a
Nothing


  paramIdents :: [Ident]
paramIdents = [ Name -> Ident
nameIdent Name
n | Just Name
n <- (TParam -> Maybe Name) -> [TParam] -> [Maybe Name]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> Maybe Name
tpName [TParam]
as ]

  -- Errors from parameters that are defined, but do not exist in the schema.
  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



-- If the instantiation contains an assignment (v := t), and the type
-- contains a free unification variable ?x that could possibly depend
-- on v, then we must require that t = v (i.e. su must be an identity
-- substitution). Otherwise, this causes a problem: If ?x is
-- eventually instantiated to a type containing v, then the type
-- substitution will have computed the wrong result.

doInst :: [(TParam, Type)] -> Expr -> [Prop] -> Type -> InferM (Expr,Type)
doInst :: [(TParam, Type)] -> Expr -> [Type] -> Type -> InferM (Expr, Type)
doInst [(TParam, Type)]
su' Expr
e [Type]
ps 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

     -- Possibly more goals due to unification
     [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
  -- Add type parameters
  addTyParams :: t Type -> Expr -> Expr
addTyParams t Type
ts 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

  -- Add proof parameters (the proofs are omitted but we mark where they'd go)
  addProofParams :: Expr -> Expr
addProofParams Expr
e1 = (Expr -> Type -> Expr) -> Expr -> [Type] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr
e2 Type
_ -> Expr -> Expr
EProofApp Expr
e2) Expr
e1 [Type]
ps

  -- free unification variables used in the schema
  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))

  -- the bound variables from the scopes of any unification variables in the schema
  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 Int
_ Kind
_ Set TParam
vs TVarInfo
_) = Set TParam
vs
      scope (TVBound TParam
_) = Set TParam
forall a. Set a
Set.empty

  -- if the tvar is in 'bounds', then make sure it is an identity substitution
  checkInst :: (TParam, Type) -> InferM [Prop]
  checkInst :: (TParam, Type) -> InferM [Type]
checkInst (TParam
tp, 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 = let a :: TVar
a   = TParam -> TVar
tpVar TParam
tp
                      src :: TypeSource
src = TVarInfo -> TypeSource
tvarDesc (TVar -> TVarInfo
tvInfo TVar
a)
                  in TypeWithSource -> Type -> InferM [Type]
unify (Type -> TypeSource -> TypeWithSource
WithSource (TVar -> Type
TVar TVar
a) TypeSource
src) Type
ty