    -- |
    -- Module      :  Cryptol.TypeCheck.Subst
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE Safe #-}
    module Cryptol.TypeCheck.Subst
      ( Subst
      , emptySubst
      , singleSubst
      , (@@)
      , defaultingSubst
      , listSubst
      , listParamSubst
      , isEmptySubst
      , FVS(..)
      , apSubstMaybe
      , TVars(..)
      , apSubstTypeMapKeys
      , substBinds
      , applySubstToVar
      , substToList
      ) where

    import           Data.Maybe
    import           Data.Either (partitionEithers)
    import qualified Data.Map.Strict as Map
    import qualified Data.IntMap as IntMap
    import           Data.Set (Set)
    import qualified Data.Set as Set

    import Cryptol.TypeCheck.AST
    import Cryptol.TypeCheck.PP
    import Cryptol.TypeCheck.TypeMap
    import qualified Cryptol.TypeCheck.SimpType as Simp
    import qualified Cryptol.TypeCheck.SimpleSolver as Simp
    import Cryptol.Utils.Panic(panic)
    import Cryptol.Utils.Misc(anyJust)

    -- | A 'Subst' value represents a substitution that maps each 'TVar'
    -- to a 'Type'.
    --
    -- Invariant: If there is a mapping from @TVFree _ _ tps _@ to a type
    -- @t@, then @t@ must not mention (directly or indirectly) any type
    -- parameter that is not in @tps@. In particular, if @t@ contains a
    -- variable @TVFree _ _ tps2 _@, then @tps2@ must be a subset of
    -- @tps@. This ensures that applying the substitution will not permit
    -- any type parameter to escape from its scope.

    data Subst = S { Subst -> IntMap (TVar, Type)
    suFreeMap :: !(IntMap.IntMap (TVar, Type))
                   , Subst -> IntMap (TVar, Type)
    suBoundMap :: !(IntMap.IntMap (TVar, Type))
                   , Subst -> Bool
    suDefaulting :: !Bool
                   }
                      deriving Int -> Subst -> ShowS
    [Subst] -> ShowS
    Subst -> String
    (Int -> Subst -> ShowS)
    -> (Subst -> String) -> ([Subst] -> ShowS) -> Show Subst
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Subst] -> ShowS
    $cshowList :: [Subst] -> ShowS
    show :: Subst -> String
    $cshow :: Subst -> String
    showsPrec :: Int -> Subst -> ShowS
    $cshowsPrec :: Int -> Subst -> ShowS
    Show

    emptySubst :: Subst
    emptySubst :: Subst
    emptySubst =
      $WS :: IntMap (TVar, Type) -> IntMap (TVar, Type) -> Bool -> Subst
    S { suFreeMap :: IntMap (TVar, Type)
    suFreeMap = IntMap (TVar, Type)
    forall a. IntMap a
    IntMap.empty
        , suBoundMap :: IntMap (TVar, Type)
    suBoundMap = IntMap (TVar, Type)
    forall a. IntMap a
    IntMap.empty
        , suDefaulting :: Bool
    suDefaulting = Bool
    False
        }

    singleSubst :: TVar -> Type -> Subst
    singleSubst :: TVar -> Type -> Subst
    singleSubst v :: TVar
    v@(TVFree i :: Int
    i _ _tps :: Set TParam
    _tps _) t :: Type
    t =
      $WS :: IntMap (TVar, Type) -> IntMap (TVar, Type) -> Bool -> Subst
    S { suFreeMap :: IntMap (TVar, Type)
    suFreeMap = Int -> (TVar, Type) -> IntMap (TVar, Type)
    forall a. Int -> a -> IntMap a
    IntMap.singleton Int
    i (TVar
    v, Type
    t)
        , suBoundMap :: IntMap (TVar, Type)
    suBoundMap = IntMap (TVar, Type)
    forall a. IntMap a
    IntMap.empty
        , suDefaulting :: Bool
    suDefaulting = Bool
    False
        }
    singleSubst v :: TVar
    v@(TVBound tp :: TParam
    tp) t :: Type
    t =
      $WS :: IntMap (TVar, Type) -> IntMap (TVar, Type) -> Bool -> Subst
    S { suFreeMap :: IntMap (TVar, Type)
    suFreeMap = IntMap (TVar, Type)
    forall a. IntMap a
    IntMap.empty
        , suBoundMap :: IntMap (TVar, Type)
    suBoundMap = Int -> (TVar, Type) -> IntMap (TVar, Type)
    forall a. Int -> a -> IntMap a
    IntMap.singleton (TParam -> Int
    tpUnique TParam
    tp) (TVar
    v, Type
    t)
        , suDefaulting :: Bool
    suDefaulting = Bool
    False
        }

    (@@) :: Subst -> Subst -> Subst
    s2 :: Subst
    s2 @@ :: Subst -> Subst -> Subst
    @@ s1 :: Subst
    s1
      | Subst -> Bool
    isEmptySubst Subst
    s2 =
        if Subst -> Bool
    suDefaulting Subst
    s1 Bool -> Bool -> Bool
    || Bool -> Bool
    not (Subst -> Bool
    suDefaulting Subst
    s2) then
          Subst
    s1
        else
          Subst
    s1{ suDefaulting :: Bool
    suDefaulting = Bool
    True }

    s2 :: Subst
    s2 @@ s1 :: Subst
    s1 =
      $WS :: IntMap (TVar, Type) -> IntMap (TVar, Type) -> Bool -> Subst
    S { suFreeMap :: IntMap (TVar, Type)
    suFreeMap = ((TVar, Type) -> (TVar, Type))
    -> IntMap (TVar, Type) -> IntMap (TVar, Type)
    forall a b. (a -> b) -> IntMap a -> IntMap b
    IntMap.map ((Type -> Type) -> (TVar, Type) -> (TVar, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    s2)) (Subst -> IntMap (TVar, Type)
    suFreeMap Subst
    s1) IntMap (TVar, Type) -> IntMap (TVar, Type) -> IntMap (TVar, Type)
    forall a. IntMap a -> IntMap a -> IntMap a
    `IntMap.union` Subst -> IntMap (TVar, Type)
    suFreeMap Subst
    s2
        , suBoundMap :: IntMap (TVar, Type)
    suBoundMap = ((TVar, Type) -> (TVar, Type))
    -> IntMap (TVar, Type) -> IntMap (TVar, Type)
    forall a b. (a -> b) -> IntMap a -> IntMap b
    IntMap.map ((Type -> Type) -> (TVar, Type) -> (TVar, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    s2)) (Subst -> IntMap (TVar, Type)
    suBoundMap Subst
    s1) IntMap (TVar, Type) -> IntMap (TVar, Type) -> IntMap (TVar, Type)
    forall a. IntMap a -> IntMap a -> IntMap a
    `IntMap.union` Subst -> IntMap (TVar, Type)
    suBoundMap Subst
    s2
        , suDefaulting :: Bool
    suDefaulting = Subst -> Bool
    suDefaulting Subst
    s1 Bool -> Bool -> Bool
    || Subst -> Bool
    suDefaulting Subst
    s2
        }

    -- | A defaulting substitution maps all otherwise-unmapped free
    -- variables to a kind-appropriate default type (@Bit@ for value types
    -- and @0@ for numeric types).
    defaultingSubst :: Subst -> Subst
    defaultingSubst :: Subst -> Subst
    defaultingSubst s :: Subst
    s = Subst
    s { suDefaulting :: Bool
    suDefaulting = Bool
    True }

    -- | Makes a substitution out of a list.
    -- WARNING: We do not validate the list in any way, so the caller should
    -- ensure that we end up with a valid (e.g., idempotent) substitution.
    listSubst :: [(TVar, Type)] -> Subst
    listSubst :: [(TVar, Type)] -> Subst
    listSubst xs :: [(TVar, Type)]
    xs
      | [(TVar, Type)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(TVar, Type)]
    xs   = Subst
    emptySubst
      | Bool
    otherwise = $WS :: IntMap (TVar, Type) -> IntMap (TVar, Type) -> Bool -> Subst
    S { suFreeMap :: IntMap (TVar, Type)
    suFreeMap = [(Int, (TVar, Type))] -> IntMap (TVar, Type)
    forall a. [(Int, a)] -> IntMap a
    IntMap.fromList [(Int, (TVar, Type))]
    frees
                      , suBoundMap :: IntMap (TVar, Type)
    suBoundMap = [(Int, (TVar, Type))] -> IntMap (TVar, Type)
    forall a. [(Int, a)] -> IntMap a
    IntMap.fromList [(Int, (TVar, Type))]
    bounds
                      , suDefaulting :: Bool
    suDefaulting = Bool
    False }
      where
        (frees :: [(Int, (TVar, Type))]
    frees, bounds :: [(Int, (TVar, Type))]
    bounds) = [Either (Int, (TVar, Type)) (Int, (TVar, Type))]
    -> ([(Int, (TVar, Type))], [(Int, (TVar, Type))])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers (((TVar, Type) -> Either (Int, (TVar, Type)) (Int, (TVar, Type)))
    -> [(TVar, Type)]
    -> [Either (Int, (TVar, Type)) (Int, (TVar, Type))]
    forall a b. (a -> b) -> [a] -> [b]
    map (TVar, Type) -> Either (Int, (TVar, Type)) (Int, (TVar, Type))
    forall b. (TVar, b) -> Either (Int, (TVar, b)) (Int, (TVar, b))
    classify [(TVar, Type)]
    xs)
        classify :: (TVar, b) -> Either (Int, (TVar, b)) (Int, (TVar, b))
    classify x :: (TVar, b)
    x =
          case (TVar, b) -> TVar
    forall a b. (a, b) -> a
    fst (TVar, b)
    x of
            TVFree i :: Int
    i _ _ _ -> (Int, (TVar, b)) -> Either (Int, (TVar, b)) (Int, (TVar, b))
    forall a b. a -> Either a b
    Left (Int
    i, (TVar, b)
    x)
            TVBound tp :: TParam
    tp -> (Int, (TVar, b)) -> Either (Int, (TVar, b)) (Int, (TVar, b))
    forall a b. b -> Either a b
    Right (TParam -> Int
    tpUnique TParam
    tp, (TVar, b)
    x)

    -- | Makes a substitution out of a list.
    -- WARNING: We do not validate the list in any way, so the caller should
    -- ensure that we end up with a valid (e.g., idempotent) substitution.
    listParamSubst :: [(TParam, Type)] -> Subst
    listParamSubst :: [(TParam, Type)] -> Subst
    listParamSubst xs :: [(TParam, Type)]
    xs
      | [(TParam, Type)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(TParam, Type)]
    xs   = Subst
    emptySubst
      | Bool
    otherwise = $WS :: IntMap (TVar, Type) -> IntMap (TVar, Type) -> Bool -> Subst
    S { suFreeMap :: IntMap (TVar, Type)
    suFreeMap = IntMap (TVar, Type)
    forall a. IntMap a
    IntMap.empty
                      , suBoundMap :: IntMap (TVar, Type)
    suBoundMap = [(Int, (TVar, Type))] -> IntMap (TVar, Type)
    forall a. [(Int, a)] -> IntMap a
    IntMap.fromList [(Int, (TVar, Type))]
    bounds
                      , suDefaulting :: Bool
    suDefaulting = Bool
    False }
      where
        bounds :: [(Int, (TVar, Type))]
    bounds = [ (TParam -> Int
    tpUnique TParam
    tp, (TParam -> TVar
    TVBound TParam
    tp, Type
    t)) | (tp :: TParam
    tp, t :: Type
    t) <- [(TParam, Type)]
    xs ]

    isEmptySubst :: Subst -> Bool
    isEmptySubst :: Subst -> Bool
    isEmptySubst su :: Subst
    su = IntMap (TVar, Type) -> Bool
    forall a. IntMap a -> Bool
    IntMap.null (Subst -> IntMap (TVar, Type)
    suFreeMap Subst
    su) Bool -> Bool -> Bool
    && IntMap (TVar, Type) -> Bool
    forall a. IntMap a -> Bool
    IntMap.null (Subst -> IntMap (TVar, Type)
    suBoundMap Subst
    su)

    -- Returns the empty set if this is a defaulting substitution
    substBinds :: Subst -> Set TVar
    substBinds :: Subst -> Set TVar
    substBinds su :: Subst
    su
      | Subst -> Bool
    suDefaulting Subst
    su = Set TVar
    forall a. Set a
    Set.empty
      | Bool
    otherwise       = [TVar] -> Set TVar
    forall a. Ord a => [a] -> Set a
    Set.fromList (((TVar, Type) -> TVar) -> [(TVar, Type)] -> [TVar]
    forall a b. (a -> b) -> [a] -> [b]
    map (TVar, Type) -> TVar
    forall a b. (a, b) -> a
    fst (Subst -> [(TVar, Type)]
    assocsSubst Subst
    su))

    substToList :: Subst -> [(TVar, Type)]
    substToList :: Subst -> [(TVar, Type)]
    substToList s :: Subst
    s
      | Subst -> Bool
    suDefaulting Subst
    s = String -> [String] -> [(TVar, Type)]
    forall a. HasCallStack => String -> [String] -> a
    panic "substToList" ["Defaulting substitution."]
      | Bool
    otherwise = Subst -> [(TVar, Type)]
    assocsSubst Subst
    s

    assocsSubst :: Subst -> [(TVar, Type)]
    assocsSubst :: Subst -> [(TVar, Type)]
    assocsSubst s :: Subst
    s = [(TVar, Type)]
    frees [(TVar, Type)] -> [(TVar, Type)] -> [(TVar, Type)]
    forall a. [a] -> [a] -> [a]
    ++ [(TVar, Type)]
    bounds
      where
        frees :: [(TVar, Type)]
    frees = IntMap (TVar, Type) -> [(TVar, Type)]
    forall a. IntMap a -> [a]
    IntMap.elems (Subst -> IntMap (TVar, Type)
    suFreeMap Subst
    s)
        bounds :: [(TVar, Type)]
    bounds = IntMap (TVar, Type) -> [(TVar, Type)]
    forall a. IntMap a -> [a]
    IntMap.elems (Subst -> IntMap (TVar, Type)
    suBoundMap Subst
    s)

    instance PP (WithNames Subst) where
      ppPrec :: Int -> WithNames Subst -> Doc
    ppPrec _ (WithNames s :: Subst
    s mp :: NameMap
    mp)
        | [(TVar, Type)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(TVar, Type)]
    els  = String -> Doc
    text "(empty substitution)"
        | Bool
    otherwise = String -> Doc
    text "Substitution:" Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest 2 ([Doc] -> Doc
    vcat (((TVar, Type) -> Doc) -> [(TVar, Type)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (TVar, Type) -> Doc
    forall a a. (PP (WithNames a), PP (WithNames a)) => (a, a) -> Doc
    pp1 [(TVar, Type)]
    els))
        where pp1 :: (a, a) -> Doc
    pp1 (x :: a
    x,t :: a
    t) = NameMap -> a -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    mp a
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text "=" Doc -> Doc -> Doc
    <+> NameMap -> a -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    mp a
    t
              els :: [(TVar, Type)]
    els       = Subst -> [(TVar, Type)]
    assocsSubst Subst
    s

    instance PP Subst where
      ppPrec :: Int -> Subst -> Doc
    ppPrec n :: Int
    n = NameMap -> Int -> Subst -> Doc
    forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
    ppWithNamesPrec NameMap
    forall a. IntMap a
    IntMap.empty Int
    n

    -- | Apply a substitution.  Returns `Nothing` if nothing changed.
    apSubstMaybe :: Subst -> Type -> Maybe Type
    apSubstMaybe :: Subst -> Type -> Maybe Type
    apSubstMaybe su :: Subst
    su ty :: Type
    ty =
      case Type
    ty of
        TCon t :: TCon
    t ts :: [Type]
    ts ->
          do [Type]
    ss <- (Type -> Maybe Type) -> [Type] -> Maybe [Type]
    forall (t :: * -> *) a.
    Traversable t =>
    (a -> Maybe a) -> t a -> Maybe (t a)
    anyJust (Subst -> Type -> Maybe Type
    apSubstMaybe Subst
    su) [Type]
    ts
             case TCon
    t of
               TF _ -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $! TCon -> [Type] -> Type
    Simp.tCon TCon
    t [Type]
    ss
               PC _ -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $! Ctxt -> Type -> Type
    Simp.simplify Ctxt
    forall k a. Map k a
    Map.empty (TCon -> [Type] -> Type
    TCon TCon
    t [Type]
    ss)
               _    -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (TCon -> [Type] -> Type
    TCon TCon
    t [Type]
    ss)

        TUser f :: Name
    f ts :: [Type]
    ts t :: Type
    t  -> do Type
    t1 <- Subst -> Type -> Maybe Type
    apSubstMaybe Subst
    su Type
    t
                            Type -> Maybe Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name -> [Type] -> Type -> Type
    TUser Name
    f ((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]
    ts) Type
    t1)
        TRec fs :: [(Ident, Type)]
    fs       -> [(Ident, Type)] -> Type
    TRec ([(Ident, Type)] -> Type) -> Maybe [(Ident, Type)] -> Maybe Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` ((Ident, Type) -> Maybe (Ident, Type))
    -> [(Ident, Type)] -> Maybe [(Ident, Type)]
    forall (t :: * -> *) a.
    Traversable t =>
    (a -> Maybe a) -> t a -> Maybe (t a)
    anyJust (Ident, Type) -> Maybe (Ident, Type)
    forall a. (a, Type) -> Maybe (a, Type)
    fld [(Ident, Type)]
    fs
          where fld :: (a, Type) -> Maybe (a, Type)
    fld (x :: a
    x,t :: Type
    t) = do Type
    t1 <- Subst -> Type -> Maybe Type
    apSubstMaybe Subst
    su Type
    t
                               (a, Type) -> Maybe (a, Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    x,Type
    t1)
        TVar x :: TVar
    x -> Subst -> TVar -> Maybe Type
    applySubstToVar Subst
    su TVar
    x

    lookupSubst :: TVar -> Subst -> Maybe Type
    lookupSubst :: TVar -> Subst -> Maybe Type
    lookupSubst x :: TVar
    x su :: Subst
    su =
      ((TVar, Type) -> Type) -> Maybe (TVar, Type) -> Maybe Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (TVar, Type) -> Type
    forall a b. (a, b) -> b
    snd (Maybe (TVar, Type) -> Maybe Type)
    -> Maybe (TVar, Type) -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $
      case TVar
    x of
        TVFree i :: Int
    i _ _ _ -> Int -> IntMap (TVar, Type) -> Maybe (TVar, Type)
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup Int
    i (Subst -> IntMap (TVar, Type)
    suFreeMap Subst
    su)
        TVBound tp :: TParam
    tp -> Int -> IntMap (TVar, Type) -> Maybe (TVar, Type)
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup (TParam -> Int
    tpUnique TParam
    tp) (Subst -> IntMap (TVar, Type)
    suBoundMap Subst
    su)

    applySubstToVar :: Subst -> TVar -> Maybe Type
    applySubstToVar :: Subst -> TVar -> Maybe Type
    applySubstToVar su :: Subst
    su x :: TVar
    x =
      case TVar -> Subst -> Maybe Type
    lookupSubst TVar
    x Subst
    su of
        -- For a defaulting substitution, we must recurse in order to
        -- replace unmapped free vars with default types.
        Just t :: Type
    t  -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (if Subst -> Bool
    suDefaulting Subst
    su then Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t else Type
    t)
        Nothing
          | Subst -> Bool
    suDefaulting Subst
    su -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $! TVar -> Type
    defaultFreeVar TVar
    x
          | Bool
    otherwise       -> Maybe Type
    forall a. Maybe a
    Nothing

    class TVars t where
      apSubst :: Subst -> t -> t      -- ^ replaces free vars

    instance TVars t => TVars (Maybe t) where
      apSubst :: Subst -> Maybe t -> Maybe t
    apSubst s :: Subst
    s       = (t -> t) -> Maybe t -> Maybe t
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Subst -> t -> t
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    s)

    instance TVars t => TVars [t] where
      apSubst :: Subst -> [t] -> [t]
    apSubst s :: Subst
    s       = (t -> t) -> [t] -> [t]
    forall a b. (a -> b) -> [a] -> [b]
    map (Subst -> t -> t
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    s)

    instance (TVars s, TVars t) => TVars (s,t) where
      apSubst :: Subst -> (s, t) -> (s, t)
    apSubst s :: Subst
    s (x :: s
    x,y :: t
    y)       = (Subst -> s -> s
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    s s
    x, Subst -> t -> t
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    s t
    y)

    instance TVars Type where
      apSubst :: Subst -> Type -> Type
    apSubst su :: Subst
    su ty :: Type
    ty = Type -> Maybe Type -> Type
    forall a. a -> Maybe a -> a
    fromMaybe Type
    ty (Subst -> Type -> Maybe Type
    apSubstMaybe Subst
    su Type
    ty)

    -- | Pick types for unconstrained unification variables.
    defaultFreeVar :: TVar -> Type
    defaultFreeVar :: TVar -> Type
    defaultFreeVar x :: TVar
    x@(TVBound {}) = TVar -> Type
    TVar TVar
    x
    defaultFreeVar (TVFree _ k :: Kind
    k _ d :: TVarInfo
    d) =
      case Kind
    k of
        KType -> Type
    tBit
        KNum  -> Int -> Type
    forall a. Integral a => a -> Type
    tNum (0 :: Int)
        _     -> String -> [String] -> Type
    forall a. HasCallStack => String -> [String] -> a
    panic "Cryptol.TypeCheck.Subst.defaultFreeVar"
                      [ "Free variable of unexpected kind."
                      , "Source: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ TVarInfo -> String
    forall a. Show a => a -> String
    show TVarInfo
    d
                      , "Kind: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    show (Kind -> Doc
    forall a. PP a => a -> Doc
    pp Kind
    k) ]

    instance (Functor m, TVars a) => TVars (List m a) where
      apSubst :: Subst -> List m a -> List m a
    apSubst su :: Subst
    su = (a -> a) -> List m a -> List m a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Subst -> a -> a
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su)

    instance TVars a => TVars (TypeMap a) where
      apSubst :: Subst -> TypeMap a -> TypeMap a
    apSubst su :: Subst
    su = (a -> a) -> TypeMap a -> TypeMap a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Subst -> a -> a
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su)

    -- | Apply the substitution to the keys of a type map.
    apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a
    apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a
    apSubstTypeMapKeys su :: Subst
    su = (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
    forall a. (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
    go (\_ x :: a
    x -> a
    x) a -> a
    forall a. a -> a
    id
      where

      go :: (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
      go :: (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
    go merge :: a -> a -> a
    merge atNode :: a -> a
    atNode TM { .. } = (TypeMap a -> (Type, a) -> TypeMap a)
    -> TypeMap a -> [(Type, a)] -> TypeMap a
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl TypeMap a -> (Type, a) -> TypeMap a
    forall (m :: * -> *) k. TrieMap m k => m a -> (k, a) -> m a
    addKey TypeMap a
    tm' [(Type, a)]
    tys
        where
        addKey :: m a -> (k, a) -> m a
    addKey tm :: m a
    tm (ty :: k
    ty,a :: a
    a) = (a -> a -> a) -> k -> a -> m a -> m a
    forall (m :: * -> *) k a.
    TrieMap m k =>
    (a -> a -> a) -> k -> a -> m a -> m a
    insertWithTM a -> a -> a
    merge k
    ty a
    a m a
    tm

        tm' :: TypeMap a
    tm' = TM :: forall a.
    Map TVar a
    -> Map TCon (List TypeMap a)
    -> Map [Ident] (List TypeMap a)
    -> TypeMap a
    TM { tvar :: Map TVar a
    tvar = [(TVar, a)] -> Map TVar a
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList   [(TVar, a)]
    vars
                 , tcon :: Map TCon (List TypeMap a)
    tcon = (List TypeMap a -> List TypeMap a)
    -> Map TCon (List TypeMap a) -> Map TCon (List TypeMap a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
    forall a.
    (a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
    lgo a -> a -> a
    merge a -> a
    atNode) Map TCon (List TypeMap a)
    tcon
                 , trec :: Map [Ident] (List TypeMap a)
    trec = (List TypeMap a -> List TypeMap a)
    -> Map [Ident] (List TypeMap a) -> Map [Ident] (List TypeMap a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
    forall a.
    (a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
    lgo a -> a -> a
    merge a -> a
    atNode) Map [Ident] (List TypeMap a)
    trec
                 }

        -- partition out variables that have been replaced with more specific types
        (vars :: [(TVar, a)]
    vars,tys :: [(Type, a)]
    tys) = [Either (TVar, a) (Type, a)] -> ([(TVar, a)], [(Type, a)])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers
                     [ case Subst -> TVar -> Maybe Type
    applySubstToVar Subst
    su TVar
    v of
                         Just ty :: Type
    ty -> (Type, a) -> Either (TVar, a) (Type, a)
    forall a b. b -> Either a b
    Right (Type
    ty,a
    a')
                         Nothing -> (TVar, a) -> Either (TVar, a) (Type, a)
    forall a b. a -> Either a b
    Left  (TVar
    v, a
    a')

                     | (v :: TVar
    v,a :: a
    a) <- Map TVar a -> [(TVar, a)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map TVar a
    tvar
                     , let a' :: a
    a' = a -> a
    atNode a
    a
                     ]

      lgo :: (a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
      lgo :: (a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
    lgo merge :: a -> a -> a
    merge atNode :: a -> a
    atNode k :: List TypeMap a
    k = List TypeMap a
    k { nil :: Maybe a
    nil  = (a -> a) -> Maybe a -> Maybe a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> a
    atNode (List TypeMap a -> Maybe a
    forall (m :: * -> *) a. List m a -> Maybe a
    nil List TypeMap a
    k)
                             , cons :: TypeMap (List TypeMap a)
    cons = (List TypeMap a -> List TypeMap a -> List TypeMap a)
    -> (List TypeMap a -> List TypeMap a)
    -> TypeMap (List TypeMap a)
    -> TypeMap (List TypeMap a)
    forall a. (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
    go ((a -> a -> a) -> List TypeMap a -> List TypeMap a -> List TypeMap a
    forall (m :: * -> *) k a.
    TrieMap m k =>
    (a -> a -> a) -> m a -> m a -> m a
    unionTM a -> a -> a
    merge)
                                         ((a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
    forall a.
    (a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
    lgo a -> a -> a
    merge a -> a
    atNode)
                                         (List TypeMap a -> TypeMap (List TypeMap a)
    forall (m :: * -> *) a. List m a -> m (List m a)
    cons List TypeMap a
    k)
                             }

    {- | This instance does not need to worry about bound variable
    capture, because we rely on the 'Subst' datatype invariant to ensure
    that variable scopes will be properly preserved. -}

    instance TVars Schema where
      apSubst :: Subst -> Schema -> Schema
    apSubst su :: Subst
    su (Forall xs :: [TParam]
    xs ps :: [Type]
    ps t :: Type
    t) = [TParam] -> [Type] -> Type -> Schema
    Forall [TParam]
    xs ((Type -> [Type]) -> [Type] -> [Type]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Type -> [Type]
    pSplitAnd (Subst -> [Type] -> [Type]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su [Type]
    ps))
                                              (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t)

    instance TVars Expr where
      apSubst :: Subst -> Expr -> Expr
    apSubst su :: Subst
    su = Expr -> Expr
    go
        where
        go :: Expr -> Expr
    go expr :: Expr
    expr =
          case Expr
    expr of
            EApp e1 :: Expr
    e1 e2 :: Expr
    e2    -> Expr -> Expr -> Expr
    EApp (Expr -> Expr
    go Expr
    e1) (Expr -> Expr
    go Expr
    e2)
            EAbs x :: Name
    x t :: Type
    t e1 :: Expr
    e1   -> Name -> Type -> Expr -> Expr
    EAbs Name
    x (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t) (Expr -> Expr
    go Expr
    e1)
            ETAbs a :: TParam
    a e :: Expr
    e     -> TParam -> Expr -> Expr
    ETAbs TParam
    a (Expr -> Expr
    go Expr
    e)
            ETApp e :: Expr
    e t :: Type
    t     -> Expr -> Type -> Expr
    ETApp (Expr -> Expr
    go Expr
    e) (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t)
            EProofAbs p :: Type
    p e :: Expr
    e -> Type -> Expr -> Expr
    EProofAbs Type
    hmm (Expr -> Expr
    go Expr
    e)
              where hmm :: Type
    hmm = case Type -> [Type]
    pSplitAnd (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    p) of
                            [p1 :: Type
    p1] -> Type
    p1
                            res :: [Type]
    res -> String -> [String] -> Type
    forall a. HasCallStack => String -> [String] -> a
    panic "apSubst@EProofAbs"
                                    [ "Predicate split or disappeared after"
                                    , "we applied a substitution."
                                    , "Predicate:"
                                    , Doc -> String
    forall a. Show a => a -> String
    show (Type -> Doc
    forall a. PP a => a -> Doc
    pp Type
    p)
                                    , "Became:"
                                    , [Doc] -> String
    forall a. Show a => a -> String
    show ((Type -> Doc) -> [Type] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Doc
    forall a. PP a => a -> Doc
    pp [Type]
    res)
                                    , "subst:"
                                    , Doc -> String
    forall a. Show a => a -> String
    show (Subst -> Doc
    forall a. PP a => a -> Doc
    pp Subst
    su)
                                    ]

            EProofApp e :: Expr
    e   -> Expr -> Expr
    EProofApp (Expr -> Expr
    go Expr
    e)

            EVar {}       -> Expr
    expr

            ETuple es :: [Expr]
    es     -> [Expr] -> Expr
    ETuple ((Expr -> Expr) -> [Expr] -> [Expr]
    forall a b. (a -> b) -> [a] -> [b]
    map Expr -> Expr
    go [Expr]
    es)
            ERec fs :: [(Ident, Expr)]
    fs       -> [(Ident, Expr)] -> Expr
    ERec [ (Ident
    f, Expr -> Expr
    go Expr
    e) | (f :: Ident
    f,e :: Expr
    e) <- [(Ident, Expr)]
    fs ]
            ESet e :: Expr
    e x :: Selector
    x v :: Expr
    v    -> Expr -> Selector -> Expr -> Expr
    ESet (Expr -> Expr
    go Expr
    e) Selector
    x (Expr -> Expr
    go Expr
    v)
            EList es :: [Expr]
    es t :: Type
    t    -> [Expr] -> Type -> Expr
    EList ((Expr -> Expr) -> [Expr] -> [Expr]
    forall a b. (a -> b) -> [a] -> [b]
    map Expr -> Expr
    go [Expr]
    es) (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t)
            ESel e :: Expr
    e s :: Selector
    s      -> Expr -> Selector -> Expr
    ESel (Expr -> Expr
    go Expr
    e) Selector
    s
            EComp len :: Type
    len t :: Type
    t e :: Expr
    e mss :: [[Match]]
    mss -> Type -> Type -> Expr -> [[Match]] -> Expr
    EComp (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    len) (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t) (Expr -> Expr
    go Expr
    e) (Subst -> [[Match]] -> [[Match]]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su [[Match]]
    mss)
            EIf e1 :: Expr
    e1 e2 :: Expr
    e2 e3 :: Expr
    e3  -> Expr -> Expr -> Expr -> Expr
    EIf (Expr -> Expr
    go Expr
    e1) (Expr -> Expr
    go Expr
    e2) (Expr -> Expr
    go Expr
    e3)

            EWhere e :: Expr
    e ds :: [DeclGroup]
    ds   -> Expr -> [DeclGroup] -> Expr
    EWhere (Expr -> Expr
    go Expr
    e) (Subst -> [DeclGroup] -> [DeclGroup]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su [DeclGroup]
    ds)

    instance TVars Match where
      apSubst :: Subst -> Match -> Match
    apSubst su :: Subst
    su (From x :: Name
    x len :: Type
    len t :: Type
    t e :: Expr
    e) = Name -> Type -> Type -> Expr -> Match
    From Name
    x (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    len) (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t) (Subst -> Expr -> Expr
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Expr
    e)
      apSubst su :: Subst
    su (Let b :: Decl
    b)      = Decl -> Match
    Let (Subst -> Decl -> Decl
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Decl
    b)

    instance TVars DeclGroup where
      apSubst :: Subst -> DeclGroup -> DeclGroup
    apSubst su :: Subst
    su (NonRecursive d :: Decl
    d) = Decl -> DeclGroup
    NonRecursive (Subst -> Decl -> Decl
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Decl
    d)
      apSubst su :: Subst
    su (Recursive ds :: [Decl]
    ds)   = [Decl] -> DeclGroup
    Recursive (Subst -> [Decl] -> [Decl]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su [Decl]
    ds)

    instance TVars Decl where
      apSubst :: Subst -> Decl -> Decl
    apSubst su :: Subst
    su d :: Decl
    d          = Decl
    d { dSignature :: Schema
    dSignature  = Subst -> Schema -> Schema
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su (Decl -> Schema
    dSignature Decl
    d)
                                , dDefinition :: DeclDef
    dDefinition = Subst -> DeclDef -> DeclDef
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su (Decl -> DeclDef
    dDefinition Decl
    d)
                                }

    instance TVars DeclDef where
      apSubst :: Subst -> DeclDef -> DeclDef
    apSubst su :: Subst
    su (DExpr e :: Expr
    e) = Expr -> DeclDef
    DExpr (Subst -> Expr -> Expr
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Expr
    e)
      apSubst _  DPrim     = DeclDef
    DPrim

    instance TVars Module where
      apSubst :: Subst -> Module -> Module
    apSubst su :: Subst
    su m :: Module
    m = Module
    m { mDecls :: [DeclGroup]
    mDecls = Subst -> [DeclGroup] -> [DeclGroup]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su (Module -> [DeclGroup]
    mDecls Module
    m) }