    -- |
    -- 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 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) {- count from 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 ]

    {- | 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 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
      -- Choose the type for type parameter `x`
      paramInst :: Int -> TParam -> InferM (TParam, Type)
    paramInst n :: Int
    n x :: 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
    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)

      -- 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@(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 ]

      -- 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 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

         -- 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 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

      -- Add proof parameters (the proofs are omitted but we mark where they'd go)
      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

      -- 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 _ _ vs :: Set TParam
    vs _) = Set TParam
    vs
          scope (TVBound _) = 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 (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