-- |
-- 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(..)
  , instantiatePCon
  ) 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 { 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 { 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 Prop
checkTyParam TypeSource
src Kind
k MaybeCheckedType
mb =
  case MaybeCheckedType
mb of
    Checked Prop
t
      | Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k'   -> Prop -> InferM Prop
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
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 Prop
newType TypeSource
src Kind
k
        where k' :: Kind
k' = Prop -> Kind
forall t. HasKind t => t -> Kind
kindOf Prop
t
    Unchecked Type Name
t -> Type Name -> Maybe Kind -> InferM Prop
checkType Type Name
t (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
k)

-- | Instantiate a pattern constructor.  Returns (A,B,C,D) where:
-- A) are the instantiations of the type parameters of the constructor
-- B) is how many proofs we would have if we had dictionaries
-- C) are the types of the fields of the constructor
-- D) is the type of the result of the constructor (i.e., what we are mathcing)
instantiatePCon :: Name -> InferM ([Type],Int,[Type],Type)
instantiatePCon :: Name -> InferM ([Prop], Int, [Prop], Prop)
instantiatePCon Name
nm =
  do VarType
vart <- Name -> InferM VarType
lookupVar Name
nm
     case VarType
vart of
       CurSCC {} -> String -> [String] -> InferM ([Prop], Int, [Prop], Prop)
forall a. HasCallStack => String -> [String] -> a
panic String
"instantiatePCon" [ String
"CurSCC"]
       ExtVar Schema
s ->
         do (Expr
e,Prop
t) <- Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Prop)
instantiateWith Name
nm (Name -> Expr
EVar Name
nm) Schema
s []
            let (Expr
_, [Prop]
tApps, Int
proofApps) = Expr -> (Expr, [Prop], Int)
splitExprInst Expr
e
                ([Prop]
fs,Prop
res) = Prop -> ([Prop], Prop)
splitFun Prop
t
            ([Prop], Int, [Prop], Prop) -> InferM ([Prop], Int, [Prop], Prop)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Prop]
tApps, Int
proofApps,[Prop]
fs,Prop
res)
  where
  splitFun :: Prop -> ([Prop], Prop)
splitFun Prop
ty =
    case Prop -> Maybe (Prop, Prop)
tIsFun Prop
ty of
      Maybe (Prop, Prop)
Nothing -> ([], Prop
ty)
      Just (Prop
a,Prop
b) -> (Prop
aProp -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
:[Prop]
as,Prop
c)
        where ([Prop]
as,Prop
c) = Prop -> ([Prop], Prop)
splitFun Prop
b

instantiateWith :: Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr,Type)
instantiateWith :: Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Prop)
instantiateWith Name
nm Expr
e Schema
s [TypeArg]
ts
  | [Located (Ident, MaybeCheckedType)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Located (Ident, MaybeCheckedType)]
named      = Name -> Expr -> Schema -> [MaybeCheckedType] -> InferM (Expr, Prop)
instantiateWithPos Name
nm Expr
e Schema
s [MaybeCheckedType]
positional
  | [MaybeCheckedType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [MaybeCheckedType]
positional = Name
-> Expr
-> Schema
-> [Located (Ident, MaybeCheckedType)]
-> InferM (Expr, Prop)
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, Prop)
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 = (thing n, tyArgType 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, Prop)
instantiateWithPos Name
nm Expr
e (Forall [TParam]
as [Prop]
ps Prop
t) [MaybeCheckedType]
ts =
  do [(TParam, Prop)]
su <- Int
-> [(TParam, Prop)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Prop)]
makeSu (Int
1::Int) [] [TParam]
as [MaybeCheckedType]
ts
     [(TParam, Prop)] -> Expr -> [Prop] -> Prop -> InferM (Expr, Prop)
doInst [(TParam, Prop)]
su Expr
e [Prop]
ps Prop
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, Prop)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Prop)]
makeSu Int
n [(TParam, Prop)]
su (TParam
q : [TParam]
qs) (MaybeCheckedType
mbty : [MaybeCheckedType]
tys)
    | Bool -> Bool
not (TParam -> Bool
isNamed TParam
q) = do (TParam, Prop)
r <- Int -> TParam -> InferM (TParam, Prop)
forall {a}. HasKind a => Int -> a -> InferM (a, Prop)
unnamed Int
n TParam
q
                           Int
-> [(TParam, Prop)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Prop)]
makeSu (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ((TParam, Prop)
r (TParam, Prop) -> [(TParam, Prop)] -> [(TParam, Prop)]
forall a. a -> [a] -> [a]
: [(TParam, Prop)]
su) [TParam]
qs (MaybeCheckedType
mbty MaybeCheckedType -> [MaybeCheckedType] -> [MaybeCheckedType]
forall a. a -> [a] -> [a]
: [MaybeCheckedType]
tys)
    | Bool
otherwise = do Prop
ty <- TypeSource -> Kind -> MaybeCheckedType -> InferM Prop
checkTyParam (Name -> Int -> TypeSource
TypeParamInstPos Name
nm Int
n) (TParam -> Kind
forall t. HasKind t => t -> Kind
kindOf TParam
q) MaybeCheckedType
mbty
                     Int
-> [(TParam, Prop)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Prop)]
makeSu (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ((TParam
q,Prop
ty) (TParam, Prop) -> [(TParam, Prop)] -> [(TParam, Prop)]
forall a. a -> [a] -> [a]
: [(TParam, Prop)]
su) [TParam]
qs [MaybeCheckedType]
tys

  makeSu Int
_ [(TParam, Prop)]
su [] []       = [(TParam, Prop)] -> InferM [(TParam, Prop)]
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TParam, Prop)] -> [(TParam, Prop)]
forall a. [a] -> [a]
reverse [(TParam, Prop)]
su)
  makeSu Int
n [(TParam, Prop)]
su (TParam
q : [TParam]
qs) [] = do (TParam, Prop)
r <- Int -> TParam -> InferM (TParam, Prop)
forall {a}. HasKind a => Int -> a -> InferM (a, Prop)
unnamed Int
n TParam
q
                               Int
-> [(TParam, Prop)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Prop)]
makeSu (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ((TParam, Prop)
r (TParam, Prop) -> [(TParam, Prop)] -> [(TParam, Prop)]
forall a. a -> [a] -> [a]
: [(TParam, Prop)]
su) [TParam]
qs []
  makeSu Int
_ [(TParam, Prop)]
su [] [MaybeCheckedType]
_        = do Error -> InferM ()
recordError Error
TooManyPositionalTypeParams
                               [(TParam, Prop)] -> InferM [(TParam, Prop)]
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TParam, Prop)] -> [(TParam, Prop)]
forall a. [a] -> [a]
reverse [(TParam, Prop)]
su)

  unnamed :: Int -> a -> InferM (a, Prop)
unnamed Int
n a
q = do Prop
ty <- TypeSource -> Kind -> InferM Prop
newType TypeSource
src (a -> Kind
forall t. HasKind t => t -> Kind
kindOf a
q)
                   (a, Prop) -> InferM (a, Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
q, Prop
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, Prop)
instantiateWithNames Name
nm Expr
e (Forall [TParam]
as [Prop]
ps Prop
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 a b. (a -> b) -> Located a -> Located b
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, Prop)]
su' <- (Int -> TParam -> InferM (TParam, Prop))
-> [Int] -> [TParam] -> InferM [(TParam, Prop)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Int -> TParam -> InferM (TParam, Prop)
paramInst [ Int
1.. ] [TParam]
as
     [(TParam, Prop)] -> Expr -> [Prop] -> Prop -> InferM (Expr, Prop)
doInst [(TParam, Prop)]
su' Expr
e [Prop]
ps Prop
t
  where
  -- Choose the type for type parameter `x`
  paramInst :: Int -> TParam -> InferM (TParam, Prop)
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
       Prop
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 Prop
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 Prop
newType TypeSource
src Kind
k
       (TParam, Prop) -> InferM (TParam, Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TParam
x, Prop
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, Prop)] -> Expr -> [Prop] -> Prop -> InferM (Expr, Prop)
doInst [(TParam, Prop)]
su' Expr
e [Prop]
ps Prop
t =
  do let su :: Subst
su = [(TParam, Prop)] -> Subst
listParamSubst [(TParam, Prop)]
su'
     ConstraintSource -> [Prop] -> InferM ()
newGoals (Expr -> ConstraintSource
CtInst Expr
e) ((Prop -> Prop) -> [Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Prop -> Prop
forall t. TVars t => Subst -> t -> t
apSubst Subst
su) [Prop]
ps)
     let t1 :: Prop
t1 = Subst -> Prop -> Prop
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Prop
t

     -- Possibly more goals due to unification
     [Prop]
ps' <- [[Prop]] -> [Prop]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Prop]] -> [Prop]) -> InferM [[Prop]] -> InferM [Prop]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((TParam, Prop) -> InferM [Prop])
-> [(TParam, Prop)] -> InferM [[Prop]]
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 (TParam, Prop) -> InferM [Prop]
checkInst [(TParam, Prop)]
su'
     ConstraintSource -> [Prop] -> InferM ()
newGoals (Expr -> ConstraintSource
CtInst Expr
e) [Prop]
ps'

     (Expr, Prop) -> InferM (Expr, Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ( Expr -> Expr
addProofParams ([Prop] -> Expr -> Expr
forall {t :: * -> *}. Foldable t => t Prop -> Expr -> Expr
addTyParams (((TParam, Prop) -> Prop) -> [(TParam, Prop)] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (TParam, Prop) -> Prop
forall a b. (a, b) -> b
snd [(TParam, Prop)]
su') Expr
e), Prop
t1 )
  where
  -- Add type parameters
  addTyParams :: t Prop -> Expr -> Expr
addTyParams t Prop
ts Expr
e1 = (Expr -> Prop -> Expr) -> Expr -> t Prop -> Expr
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Prop -> Expr
ETApp Expr
e1 t Prop
ts

  -- Add proof parameters (the proofs are omitted but we mark where they'd go)
  addProofParams :: Expr -> Expr
addProofParams Expr
e1 = (Expr -> Prop -> Expr) -> Expr -> [Prop] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr
e2 Prop
_ -> Expr -> Expr
EProofApp Expr
e2) Expr
e1 [Prop]
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 ((Prop -> Set TVar) -> [Prop] -> [Set TVar]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (Prop
t Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: [Prop]
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, Prop) -> InferM [Prop]
checkInst (TParam
tp, Prop
ty)
    | TParam -> Set TParam -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember TParam
tp Set TParam
bounds = [Prop] -> InferM [Prop]
forall a. a -> InferM a
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)
                      rng :: Maybe Range
rng = Range -> Maybe Range
forall a. a -> Maybe a
Just (TVarInfo -> Range
tvarSource (TVar -> TVarInfo
tvInfo TVar
a))
                  in TypeWithSource -> Prop -> InferM [Prop]
unify (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource (TVar -> Prop
TVar TVar
a) TypeSource
src Maybe Range
rng) Prop
ty