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

    {-# LANGUAGE BangPatterns #-}
    {-# LANGUAGE DeriveTraversable #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE Safe #-}
    module Cryptol.TypeCheck.Subst
      ( Subst
      , emptySubst
      , SubstError(..)
      , singleSubst
      , singleTParamSubst
      , uncheckedSingleSubst
      , (@@)
      , defaultingSubst
      , listSubst
      , listParamSubst
      , isEmptySubst
      , FVS(..)
      , apSubstMaybe
      , TVars(..)
      , apSubstTypeMapKeys
      , substBinds
      , applySubstToVar
      , substToList
      , fmap', (!$), (.$)
      , mergeDistinctSubst
      ) 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, anyJust2)

    -- | A 'Subst' value represents a substitution that maps each 'TVar'
    -- to a 'Type'.
    --
    -- Invariant 1: 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.
    --
    -- Invariant 2: The substitution must be idempotent, in that applying
    -- a substitution to any 'Type' in the map should leave that 'Type'
    -- unchanged. In other words, 'Type' values in the range of a 'Subst'
    -- should not mention any 'TVar' in the domain of the 'Subst'. In
    -- particular, this implies that a substitution must not contain any
    -- recursive variable mappings.
    --
    -- Invariant 3: The substitution must be kind correct: Each 'TVar' in
    -- the substitution must map to a 'Type' of the same kind.

    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
    $cshowsPrec :: Int -> Subst -> ShowS
    showsPrec :: Int -> Subst -> ShowS
    $cshow :: Subst -> String
    show :: Subst -> String
    $cshowList :: [Subst] -> ShowS
    showList :: [Subst] -> ShowS
    Show

    emptySubst :: Subst
    emptySubst :: Subst
    emptySubst =
      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
        }

    mergeDistinctSubst :: [Subst] -> Subst
    mergeDistinctSubst :: [Subst] -> Subst
    mergeDistinctSubst [Subst]
    sus =
      case [Subst]
    sus of
        [] -> Subst
    emptySubst
        [Subst]
    _  -> (Subst -> Subst -> Subst) -> [Subst] -> Subst
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 Subst -> Subst -> Subst
    merge [Subst]
    sus

      where
      merge :: Subst -> Subst -> Subst
    merge Subst
    s1 Subst
    s2 = S { suFreeMap :: IntMap (TVar, Type)
    suFreeMap     = (Subst -> IntMap (TVar, Type))
    -> Subst -> Subst -> IntMap (TVar, Type)
    forall {t} {a}. (t -> IntMap a) -> t -> t -> IntMap a
    jn Subst -> IntMap (TVar, Type)
    suFreeMap Subst
    s1 Subst
    s2
                      , suBoundMap :: IntMap (TVar, Type)
    suBoundMap    = (Subst -> IntMap (TVar, Type))
    -> Subst -> Subst -> IntMap (TVar, Type)
    forall {t} {a}. (t -> IntMap a) -> t -> t -> IntMap a
    jn Subst -> IntMap (TVar, Type)
    suBoundMap Subst
    s1 Subst
    s2
                      , suDefaulting :: Bool
    suDefaulting  = if Subst -> Bool
    suDefaulting Subst
    s1 Bool -> Bool -> Bool
    || Subst -> Bool
    suDefaulting Subst
    s2
                                          then Bool
    forall {a}. a
    err
                                          else Bool
    False
                      }

      err :: a
    err       = String -> [String] -> a
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "mergeDistinctSubst" [ String
    "Not distinct" ]
      bad :: p -> p -> a
    bad p
    _ p
    _   = a
    forall {a}. a
    err
      jn :: (t -> IntMap a) -> t -> t -> IntMap a
    jn t -> IntMap a
    f t
    x t
    y  = (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
    forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
    IntMap.unionWith a -> a -> a
    forall {p} {p} {a}. p -> p -> a
    bad (t -> IntMap a
    f t
    x) (t -> IntMap a
    f t
    y)

    -- | Reasons to reject a single-variable substitution.
    data SubstError
      = SubstRecursive
      -- ^ 'TVar' maps to a type containing the same variable.
      | SubstEscaped [TParam]
      -- ^ 'TVar' maps to a type containing one or more out-of-scope bound variables.
      | SubstKindMismatch Kind Kind
      -- ^ 'TVar' maps to a type with a different kind.

    singleSubst :: TVar -> Type -> Either SubstError Subst
    singleSubst :: TVar -> Type -> Either SubstError Subst
    singleSubst TVar
    x Type
    t
      | TVar -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TVar
    x Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Type -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Type
    t   = SubstError -> Either SubstError Subst
    forall a b. a -> Either a b
    Left (Kind -> Kind -> SubstError
    SubstKindMismatch (TVar -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TVar
    x) (Type -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Type
    t))
      | TVar
    x TVar -> Set TVar -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Type -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Type
    t   = SubstError -> Either SubstError Subst
    forall a b. a -> Either a b
    Left SubstError
    SubstRecursive
      | Bool -> Bool
    not (Set TParam -> Bool
    forall a. Set a -> Bool
    Set.null Set TParam
    escaped) = SubstError -> Either SubstError Subst
    forall a b. a -> Either a b
    Left ([TParam] -> SubstError
    SubstEscaped (Set TParam -> [TParam]
    forall a. Set a -> [a]
    Set.toList Set TParam
    escaped))
      | Bool
    otherwise              = Subst -> Either SubstError Subst
    forall a b. b -> Either a b
    Right (TVar -> Type -> Subst
    uncheckedSingleSubst TVar
    x Type
    t)
      where
        escaped :: Set TParam
    escaped =
          case TVar
    x of
            TVBound TParam
    _ -> Set TParam
    forall a. Set a
    Set.empty
            TVFree Int
    _ Kind
    _ Set TParam
    scope TVarInfo
    _ -> Type -> Set TParam
    forall t. FVS t => t -> Set TParam
    freeParams Type
    t Set TParam -> Set TParam -> Set TParam
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.difference` Set TParam
    scope

    uncheckedSingleSubst :: TVar -> Type -> Subst
    uncheckedSingleSubst :: TVar -> Type -> Subst
    uncheckedSingleSubst v :: TVar
    v@(TVFree Int
    i Kind
    _ Set TParam
    _tps TVarInfo
    _) Type
    t =
      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
        }
    uncheckedSingleSubst v :: TVar
    v@(TVBound TParam
    tp) Type
    t =
      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
        }

    singleTParamSubst :: TParam -> Type -> Subst
    singleTParamSubst :: TParam -> Type -> Subst
    singleTParamSubst TParam
    tp Type
    t = TVar -> Type -> Subst
    uncheckedSingleSubst (TParam -> TVar
    TVBound TParam
    tp) Type
    t

    (@@) :: Subst -> Subst -> Subst
    Subst
    s2 @@ :: Subst -> Subst -> Subst
    @@ 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 }

    Subst
    s2 @@ Subst
    s1 =
      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 a b. (a -> b) -> (TVar, a) -> (TVar, b)
    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 a b. (a -> b) -> (TVar, a) -> (TVar, b)
    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 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 [(TVar, Type)]
    xs
      | [(TVar, Type)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(TVar, Type)]
    xs   = Subst
    emptySubst
      | Bool
    otherwise = 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
        ([(Int, (TVar, Type))]
    frees, [(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 (TVar, b)
    x =
          case (TVar, b) -> TVar
    forall a b. (a, b) -> a
    fst (TVar, b)
    x of
            TVFree Int
    i Kind
    _ Set TParam
    _ TVarInfo
    _ -> (Int, (TVar, b)) -> Either (Int, (TVar, b)) (Int, (TVar, b))
    forall a b. a -> Either a b
    Left (Int
    i, (TVar, b)
    x)
            TVBound 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 [(TParam, Type)]
    xs
      | [(TParam, Type)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(TParam, Type)]
    xs   = Subst
    emptySubst
      | Bool
    otherwise = 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)) | (TParam
    tp, Type
    t) <- [(TParam, Type)]
    xs ]

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

    assocsSubst :: Subst -> [(TVar, Type)]
    assocsSubst :: Subst -> [(TVar, Type)]
    assocsSubst 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 Int
    _ (WithNames Subst
    s NameMap
    mp)
        | [(TVar, Type)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(TVar, Type)]
    els  = String -> Doc
    text String
    "(empty substitution)"
        | Bool
    otherwise = String -> Doc
    text String
    "Substitution:" Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest Int
    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 (a
    x,a
    t) = NameMap -> a -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    mp a
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "=" 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 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

    infixl 0 !$
    infixl 0 .$

    -- | Left-associative variant of the strict application operator '$!'.
    (!$) :: (a -> b) -> a -> b
    !$ :: forall a b. (a -> b) -> a -> b
    (!$) = (a -> b) -> a -> b
    forall a b. (a -> b) -> a -> b
    ($!)

    -- | Left-associative variant of the application operator '$'.
    (.$) :: (a -> b) -> a -> b
    .$ :: forall a b. (a -> b) -> a -> b
    (.$) = (a -> b) -> a -> b
    forall a b. (a -> b) -> a -> b
    ($)

    -- Only used internally to define fmap'.
    data Done a = Done a
      deriving ((forall a b. (a -> b) -> Done a -> Done b)
    -> (forall a b. a -> Done b -> Done a) -> Functor Done
    forall a b. a -> Done b -> Done a
    forall a b. (a -> b) -> Done a -> Done b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Done a -> Done b
    fmap :: forall a b. (a -> b) -> Done a -> Done b
    $c<$ :: forall a b. a -> Done b -> Done a
    <$ :: forall a b. a -> Done b -> Done a
    Functor, (forall m. Monoid m => Done m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Done a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Done a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Done a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Done a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Done a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Done a -> b)
    -> (forall a. (a -> a -> a) -> Done a -> a)
    -> (forall a. (a -> a -> a) -> Done a -> a)
    -> (forall a. Done a -> [a])
    -> (forall a. Done a -> Bool)
    -> (forall a. Done a -> Int)
    -> (forall a. Eq a => a -> Done a -> Bool)
    -> (forall a. Ord a => Done a -> a)
    -> (forall a. Ord a => Done a -> a)
    -> (forall a. Num a => Done a -> a)
    -> (forall a. Num a => Done a -> a)
    -> Foldable Done
    forall a. Eq a => a -> Done a -> Bool
    forall a. Num a => Done a -> a
    forall a. Ord a => Done a -> a
    forall m. Monoid m => Done m -> m
    forall a. Done a -> Bool
    forall a. Done a -> Int
    forall a. Done a -> [a]
    forall a. (a -> a -> a) -> Done a -> a
    forall m a. Monoid m => (a -> m) -> Done a -> m
    forall b a. (b -> a -> b) -> b -> Done a -> b
    forall a b. (a -> b -> b) -> b -> Done a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => Done m -> m
    fold :: forall m. Monoid m => Done m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Done a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Done a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Done a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Done a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Done a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Done a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Done a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Done a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Done a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Done a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Done a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Done a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Done a -> a
    foldr1 :: forall a. (a -> a -> a) -> Done a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Done a -> a
    foldl1 :: forall a. (a -> a -> a) -> Done a -> a
    $ctoList :: forall a. Done a -> [a]
    toList :: forall a. Done a -> [a]
    $cnull :: forall a. Done a -> Bool
    null :: forall a. Done a -> Bool
    $clength :: forall a. Done a -> Int
    length :: forall a. Done a -> Int
    $celem :: forall a. Eq a => a -> Done a -> Bool
    elem :: forall a. Eq a => a -> Done a -> Bool
    $cmaximum :: forall a. Ord a => Done a -> a
    maximum :: forall a. Ord a => Done a -> a
    $cminimum :: forall a. Ord a => Done a -> a
    minimum :: forall a. Ord a => Done a -> a
    $csum :: forall a. Num a => Done a -> a
    sum :: forall a. Num a => Done a -> a
    $cproduct :: forall a. Num a => Done a -> a
    product :: forall a. Num a => Done a -> a
    Foldable, Functor Done
    Foldable Done
    Functor Done
    -> Foldable Done
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> Done a -> f (Done b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Done (f a) -> f (Done a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Done a -> m (Done b))
    -> (forall (m :: * -> *) a. Monad m => Done (m a) -> m (Done a))
    -> Traversable Done
    forall (t :: * -> *).
    Functor t
    -> Foldable t
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a. Monad m => Done (m a) -> m (Done a)
    forall (f :: * -> *) a. Applicative f => Done (f a) -> f (Done a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Done a -> m (Done b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Done a -> f (Done b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Done a -> f (Done b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Done a -> f (Done b)
    $csequenceA :: forall (f :: * -> *) a. Applicative f => Done (f a) -> f (Done a)
    sequenceA :: forall (f :: * -> *) a. Applicative f => Done (f a) -> f (Done a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Done a -> m (Done b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Done a -> m (Done b)
    $csequence :: forall (m :: * -> *) a. Monad m => Done (m a) -> m (Done a)
    sequence :: forall (m :: * -> *) a. Monad m => Done (m a) -> m (Done a)
    Traversable)

    instance Applicative Done where
      pure :: forall a. a -> Done a
    pure a
    x = a -> Done a
    forall a. a -> Done a
    Done a
    x
      Done a -> b
    f <*> :: forall a b. Done (a -> b) -> Done a -> Done b
    <*> Done a
    x = b -> Done b
    forall a. a -> Done a
    Done (a -> b
    f a
    x)

    -- | Strict variant of 'fmap'.
    fmap' :: Traversable t => (a -> b) -> t a -> t b
    fmap' :: forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
    fmap' a -> b
    f t a
    xs = case (a -> Done b) -> t a -> Done (t b)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b)
    traverse a -> Done b
    f' t a
    xs of Done t b
    y -> t b
    y
      where f' :: a -> Done b
    f' a
    x = b -> Done b
    forall a. a -> Done a
    Done (b -> Done b) -> b -> Done b
    forall a b. (a -> b) -> a -> b
    $! a -> b
    f a
    x

    -- | Apply a substitution.  Returns `Nothing` if nothing changed.
    apSubstMaybe :: Subst -> Type -> Maybe Type
    apSubstMaybe :: Subst -> Type -> Maybe Type
    apSubstMaybe Subst
    su Type
    ty =
      case Type
    ty of
        TCon TCon
    t [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 TFun
    _ -> 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 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 a. Monoid a => a
    mempty (TCon -> [Type] -> Type
    TCon TCon
    t [Type]
    ss)
               TCon
    _    -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (TCon -> [Type] -> Type
    TCon TCon
    t [Type]
    ss)

        TUser Name
    f [Type]
    ts Type
    t ->
          do ([Type]
    ts1, Type
    t1) <- ([Type] -> Maybe [Type])
    -> (Type -> Maybe Type) -> ([Type], Type) -> Maybe ([Type], Type)
    forall a b.
    (a -> Maybe a) -> (b -> Maybe b) -> (a, b) -> Maybe (a, b)
    anyJust2 ((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)) (Subst -> Type -> Maybe Type
    apSubstMaybe Subst
    su) ([Type]
    ts, Type
    t)
             Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Name -> [Type] -> Type -> Type
    TUser Name
    f [Type]
    ts1 Type
    t1)

        TRec RecordMap Ident Type
    fs -> RecordMap Ident Type -> Type
    TRec (RecordMap Ident Type -> Type)
    -> Maybe (RecordMap Ident Type) -> Maybe Type
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` ((Type -> Maybe Type)
    -> RecordMap Ident Type -> Maybe (RecordMap Ident Type)
    forall (t :: * -> *) a.
    Traversable t =>
    (a -> Maybe a) -> t a -> Maybe (t a)
    anyJust (Subst -> Type -> Maybe Type
    apSubstMaybe Subst
    su) RecordMap Ident Type
    fs)

        {- We apply the substitution to the newtype as well, because it might
        contain module parameters, which need to be substituted when
        instantiating a functor. -}
        TNewtype Newtype
    nt [Type]
    ts ->
          (Newtype -> [Type] -> Type) -> (Newtype, [Type]) -> Type
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Newtype -> [Type] -> Type
    TNewtype ((Newtype, [Type]) -> Type)
    -> Maybe (Newtype, [Type]) -> Maybe Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Newtype -> Maybe Newtype)
    -> ([Type] -> Maybe [Type])
    -> (Newtype, [Type])
    -> Maybe (Newtype, [Type])
    forall a b.
    (a -> Maybe a) -> (b -> Maybe b) -> (a, b) -> Maybe (a, b)
    anyJust2 (Subst -> Newtype -> Maybe Newtype
    applySubstToNewtype Subst
    su)
                                        ((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))
                                        (Newtype
    nt,[Type]
    ts)

        TVar TVar
    x -> Subst -> TVar -> Maybe Type
    applySubstToVar Subst
    su TVar
    x

    lookupSubst :: TVar -> Subst -> Maybe Type
    lookupSubst :: TVar -> Subst -> Maybe Type
    lookupSubst TVar
    x Subst
    su =
      ((TVar, Type) -> Type) -> Maybe (TVar, Type) -> Maybe Type
    forall a b. (a -> b) -> Maybe a -> Maybe b
    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 Int
    i Kind
    _ Set TParam
    _ TVarInfo
    _ -> 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 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 Subst
    su 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 Type
    t
          | 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
    $! Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t
          | Bool
    otherwise       -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just Type
    t
        Maybe Type
    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

    applySubstToNewtype :: Subst -> Newtype -> Maybe Newtype
    applySubstToNewtype :: Subst -> Newtype -> Maybe Newtype
    applySubstToNewtype Subst
    su Newtype
    nt =
      do ([Type]
    cs,RecordMap Ident Type
    fs) <- ([Type] -> Maybe [Type])
    -> (RecordMap Ident Type -> Maybe (RecordMap Ident Type))
    -> ([Type], RecordMap Ident Type)
    -> Maybe ([Type], RecordMap Ident Type)
    forall a b.
    (a -> Maybe a) -> (b -> Maybe b) -> (a, b) -> Maybe (a, b)
    anyJust2
                      ((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 -> Maybe Type)
    -> RecordMap Ident Type -> Maybe (RecordMap Ident Type)
    forall (t :: * -> *) a.
    Traversable t =>
    (a -> Maybe a) -> t a -> Maybe (t a)
    anyJust (Subst -> Type -> Maybe Type
    apSubstMaybe Subst
    su))
                      (Newtype -> [Type]
    ntConstraints Newtype
    nt, Newtype -> RecordMap Ident Type
    ntFields Newtype
    nt)
         Newtype -> Maybe Newtype
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Newtype
    nt { ntConstraints :: [Type]
    ntConstraints = [Type]
    cs, ntFields :: RecordMap Ident Type
    ntFields = RecordMap Ident Type
    fs }

    class TVars t where
      apSubst :: Subst -> t -> t
      -- ^ Replaces free variables. To prevent space leaks when used with
      -- large 'Subst' values, every instance of 'apSubst' should satisfy
      -- a strictness property: Forcing evaluation of @'apSubst' s x@
      -- should also force the evaluation of all recursive calls to
      -- @'apSubst' s@. This ensures that unevaluated thunks will not
      -- cause 'Subst' values to be retained on the heap.

    instance TVars t => TVars (Maybe t) where
      apSubst :: Subst -> Maybe t -> Maybe t
    apSubst Subst
    s = (t -> t) -> Maybe t -> Maybe t
    forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t 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 Subst
    s = (t -> t) -> [t] -> [t]
    forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
    fmap' (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 Subst
    s (s
    x, t
    y) = (,) (s -> t -> (s, t)) -> s -> t -> (s, t)
    forall a b. (a -> b) -> a -> b
    !$ Subst -> s -> s
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    s s
    x (t -> (s, t)) -> t -> (s, t)
    forall a b. (a -> b) -> a -> b
    !$ Subst -> t -> t
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    s t
    y

    instance TVars Type where
      apSubst :: Subst -> Type -> Type
    apSubst Subst
    su 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 Int
    _ Kind
    k Set TParam
    _ TVarInfo
    d) =
      case Kind
    k of
        Kind
    KType -> Type
    tBit
        Kind
    KNum  -> Int -> Type
    forall a. Integral a => a -> Type
    tNum (Int
    0 :: Int)
        Kind
    _     -> String -> [String] -> Type
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Cryptol.TypeCheck.Subst.defaultFreeVar"
                      [ String
    "Free variable of unexpected kind."
                      , String
    "Source: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ TVarInfo -> String
    forall a. Show a => a -> String
    show TVarInfo
    d
                      , String
    "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 (Traversable m, TVars a) => TVars (List m a) where
      apSubst :: Subst -> List m a -> List m a
    apSubst Subst
    su = (a -> a) -> List m a -> List m a
    forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t 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 Subst
    su = (a -> a) -> TypeMap a -> TypeMap a
    forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t 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 :: forall a. Subst -> TypeMap a -> TypeMap a
    apSubstTypeMapKeys Subst
    su = (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
    forall a. (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
    go (\a
    _ a
    x -> a
    x) a -> a
    forall a. a -> a
    id
      where

      go :: (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
      go :: forall a. (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
    go a -> a -> a
    merge a -> a
    atNode TM { Map [Ident] (List TypeMap a)
    Map TCon (List TypeMap a)
    Map Newtype (List TypeMap a)
    Map TVar a
    tvar :: Map TVar a
    tcon :: Map TCon (List TypeMap a)
    trec :: Map [Ident] (List TypeMap a)
    tnewtype :: Map Newtype (List TypeMap a)
    tvar :: forall a. TypeMap a -> Map TVar a
    tcon :: forall a. TypeMap a -> Map TCon (List TypeMap a)
    trec :: forall a. TypeMap a -> Map [Ident] (List TypeMap a)
    tnewtype :: forall a. TypeMap a -> Map Newtype (List TypeMap a)
    .. } = (TypeMap a -> (Type, a) -> TypeMap a)
    -> TypeMap a -> [(Type, a)] -> TypeMap a
    forall b a. (b -> a -> b) -> b -> [a] -> b
    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 m a
    tm (k
    ty,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 { 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 a b. (a -> b) -> Map TCon a -> Map TCon b
    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 a b. (a -> b) -> Map [Ident] a -> Map [Ident] b
    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
                 , tnewtype :: Map Newtype (List TypeMap a)
    tnewtype = (List TypeMap a -> List TypeMap a)
    -> Map Newtype (List TypeMap a) -> Map Newtype (List TypeMap a)
    forall a b. (a -> b) -> Map Newtype a -> Map Newtype b
    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 Newtype (List TypeMap a)
    tnewtype
                 }

        -- partition out variables that have been replaced with more specific types
        ([(TVar, a)]
    vars,[(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 Type
    ty -> (Type, a) -> Either (TVar, a) (Type, a)
    forall a b. b -> Either a b
    Right (Type
    ty,a
    a')
                         Maybe Type
    Nothing -> (TVar, a) -> Either (TVar, a) (Type, a)
    forall a b. a -> Either a b
    Left  (TVar
    v, a
    a')

                     | (TVar
    v,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 :: forall a.
    (a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
    lgo a -> a -> a
    merge a -> a
    atNode List TypeMap a
    k = List TypeMap a
    k { nil :: Maybe a
    nil  = (a -> a) -> Maybe a -> Maybe a
    forall a b. (a -> b) -> Maybe a -> Maybe b
    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 a.
    (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)
                             }

    instance TVars a => TVars (Map.Map k a) where
      -- NB, strict map
      apSubst :: Subst -> Map k a -> Map k a
    apSubst Subst
    su Map k a
    m = (a -> a) -> Map k a -> Map k a
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map (Subst -> a -> a
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su) Map k a
    m

    instance TVars TySyn where
      apSubst :: Subst -> TySyn -> TySyn
    apSubst Subst
    su (TySyn Name
    nm [TParam]
    params [Type]
    props Type
    t Maybe Text
    doc) =
        (\[Type]
    props' Type
    t' -> Name -> [TParam] -> [Type] -> Type -> Maybe Text -> TySyn
    TySyn Name
    nm [TParam]
    params [Type]
    props' Type
    t' Maybe Text
    doc)
          ([Type] -> Type -> TySyn) -> [Type] -> Type -> TySyn
    forall a b. (a -> b) -> a -> b
    !$ Subst -> [Type] -> [Type]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su [Type]
    props (Type -> TySyn) -> Type -> TySyn
    forall a b. (a -> b) -> a -> b
    !$ Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t

    {- | 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 Subst
    su (Forall [TParam]
    xs [Type]
    ps Type
    t) =
        [TParam] -> [Type] -> Type -> Schema
    Forall [TParam]
    xs ([Type] -> Type -> Schema) -> [Type] -> Type -> Schema
    forall a b. (a -> b) -> a -> b
    !$ ((Type -> Type) -> [Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Type
    doProp [Type]
    ps) (Type -> Schema) -> Type -> Schema
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t)
        where
        doProp :: Type -> Type
    doProp = [Type] -> Type
    pAnd ([Type] -> Type) -> (Type -> [Type]) -> Type -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> [Type]
    pSplitAnd (Type -> [Type]) -> (Type -> Type) -> Type -> [Type]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su
        {- NOTE: when applying a substitution to the predicates of a schema
           we preserve the number of predicate, even if some of them became
           "True" or and "And".  This is to accomodate applying substitution
           to already type checked code (e.g., when instantiating a functor)
           where the predictes in the schema need to match the corresponding
           EProofAbs in the term.
        -}

    instance TVars Expr where
      apSubst :: Subst -> Expr -> Expr
    apSubst Subst
    su = Expr -> Expr
    go
        where
        go :: Expr -> Expr
    go Expr
    expr =
          case Expr
    expr of
            ELocated Range
    r Expr
    e  -> Range -> Expr -> Expr
    ELocated Range
    r (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Expr -> Expr
    go Expr
    e)
            EApp Expr
    e1 Expr
    e2    -> Expr -> Expr -> Expr
    EApp (Expr -> Expr -> Expr) -> Expr -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Expr -> Expr
    go Expr
    e1) (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Expr -> Expr
    go Expr
    e2)
            EAbs Name
    x Type
    t Expr
    e1   -> Name -> Type -> Expr -> Expr
    EAbs Name
    x (Type -> Expr -> Expr) -> Type -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t) (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Expr -> Expr
    go Expr
    e1)
            ETAbs TParam
    a Expr
    e     -> TParam -> Expr -> Expr
    ETAbs TParam
    a (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Expr -> Expr
    go Expr
    e)
            ETApp Expr
    e Type
    t     -> Expr -> Type -> Expr
    ETApp (Expr -> Type -> Expr) -> Expr -> Type -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Expr -> Expr
    go Expr
    e) (Type -> Expr) -> Type -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t)
            EProofAbs Type
    p Expr
    e -> Type -> Expr -> Expr
    EProofAbs (Type -> Expr -> Expr) -> Type -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ Type
    p' (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Expr -> Expr
    go Expr
    e)
              where p' :: Type
    p' = [Type] -> Type
    pAnd (Type -> [Type]
    pSplitAnd (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    p))
              {- NOTE: we used to panic if `pSplitAnd` didn't return a single result.
              It is useful to avoid the panic if applying the substitution to
              already type checked code (e.g., when we are instantitaing a
              functor).  In that case, we don't have the option to modify the
              `EProofAbs` because we'd have to change all call sites, but things might
              simplify because of the extra info in the substitution. -}

            EProofApp Expr
    e   -> Expr -> Expr
    EProofApp (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Expr -> Expr
    go Expr
    e)

            EVar {}       -> Expr
    expr

            ETuple [Expr]
    es     -> [Expr] -> Expr
    ETuple ([Expr] -> Expr) -> [Expr] -> Expr
    forall a b. (a -> b) -> a -> b
    !$ ((Expr -> Expr) -> [Expr] -> [Expr]
    forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
    fmap' Expr -> Expr
    go [Expr]
    es)
            ERec RecordMap Ident Expr
    fs       -> RecordMap Ident Expr -> Expr
    ERec (RecordMap Ident Expr -> Expr) -> RecordMap Ident Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ ((Expr -> Expr) -> RecordMap Ident Expr -> RecordMap Ident Expr
    forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
    fmap' Expr -> Expr
    go RecordMap Ident Expr
    fs)
            ESet Type
    ty Expr
    e Selector
    x Expr
    v -> Type -> Expr -> Selector -> Expr -> Expr
    ESet (Type -> Expr -> Selector -> Expr -> Expr)
    -> Type -> Expr -> Selector -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    ty) (Expr -> Selector -> Expr -> Expr)
    -> Expr -> Selector -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Expr -> Expr
    go Expr
    e) (Selector -> Expr -> Expr) -> Selector -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    .$ Selector
    x (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Expr -> Expr
    go Expr
    v)
            EList [Expr]
    es Type
    t    -> [Expr] -> Type -> Expr
    EList ([Expr] -> Type -> Expr) -> [Expr] -> Type -> Expr
    forall a b. (a -> b) -> a -> b
    !$ ((Expr -> Expr) -> [Expr] -> [Expr]
    forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
    fmap' Expr -> Expr
    go [Expr]
    es) (Type -> Expr) -> Type -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t)
            ESel Expr
    e Selector
    s      -> Expr -> Selector -> Expr
    ESel (Expr -> Selector -> Expr) -> Expr -> Selector -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Expr -> Expr
    go Expr
    e) (Selector -> Expr) -> Selector -> Expr
    forall a b. (a -> b) -> a -> b
    .$ Selector
    s
            EComp Type
    len Type
    t Expr
    e [[Match]]
    mss -> Type -> Type -> Expr -> [[Match]] -> Expr
    EComp (Type -> Type -> Expr -> [[Match]] -> Expr)
    -> Type -> Type -> Expr -> [[Match]] -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    len) (Type -> Expr -> [[Match]] -> Expr)
    -> Type -> Expr -> [[Match]] -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t) (Expr -> [[Match]] -> Expr) -> Expr -> [[Match]] -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Expr -> Expr
    go Expr
    e) ([[Match]] -> Expr) -> [[Match]] -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> [[Match]] -> [[Match]]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su [[Match]]
    mss)
            EIf Expr
    e1 Expr
    e2 Expr
    e3  -> Expr -> Expr -> Expr -> Expr
    EIf (Expr -> Expr -> Expr -> Expr) -> Expr -> Expr -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Expr -> Expr
    go Expr
    e1) (Expr -> Expr -> Expr) -> Expr -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Expr -> Expr
    go Expr
    e2) (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (Expr -> Expr
    go Expr
    e3)

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

            EPropGuards [([Type], Expr)]
    guards Type
    ty -> [([Type], Expr)] -> Type -> Expr
    EPropGuards ([([Type], Expr)] -> Type -> Expr)
    -> [([Type], Expr)] -> Type -> Expr
    forall a b. (a -> b) -> a -> b
    !$ (\([Type]
    props, Expr
    e) -> (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su (Type -> Type) -> [Type] -> [Type]
    forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
    `fmap'` [Type]
    props, Subst -> Expr -> Expr
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Expr
    e)) (([Type], Expr) -> ([Type], Expr))
    -> [([Type], Expr)] -> [([Type], Expr)]
    forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
    `fmap'` [([Type], Expr)]
    guards (Type -> Expr) -> Type -> Expr
    forall a b. (a -> b) -> a -> b
    .$ Type
    ty

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

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

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

    instance TVars DeclDef where
      apSubst :: Subst -> DeclDef -> DeclDef
    apSubst Subst
    su (DExpr Expr
    e)    = Expr -> DeclDef
    DExpr (Expr -> DeclDef) -> Expr -> DeclDef
    forall a b. (a -> b) -> a -> b
    !$ (Subst -> Expr -> Expr
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Expr
    e)
      apSubst Subst
    _  DeclDef
    DPrim        = DeclDef
    DPrim
      apSubst Subst
    _  (DForeign FFIFunType
    t) = FFIFunType -> DeclDef
    DForeign FFIFunType
    t

    -- WARNING: This applies the substitution only to the declarations.
    instance TVars (ModuleG names) where
      apSubst :: Subst -> ModuleG names -> ModuleG names
    apSubst Subst
    su ModuleG names
    m =
        let !decls' :: [DeclGroup]
    decls' = Subst -> [DeclGroup] -> [DeclGroup]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su (ModuleG names -> [DeclGroup]
    forall mname. ModuleG mname -> [DeclGroup]
    mDecls ModuleG names
    m)
            !funs' :: Map Name (ModuleG Name)
    funs'  = Subst -> ModuleG Name -> ModuleG Name
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su (ModuleG Name -> ModuleG Name)
    -> Map Name (ModuleG Name) -> Map Name (ModuleG Name)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleG names -> Map Name (ModuleG Name)
    forall mname. ModuleG mname -> Map Name (ModuleG Name)
    mFunctors ModuleG names
    m
        in ModuleG names
    m { mDecls :: [DeclGroup]
    mDecls = [DeclGroup]
    decls', mFunctors :: Map Name (ModuleG Name)
    mFunctors = Map Name (ModuleG Name)
    funs' }

    -- WARNING: This applies the substitution only to the declarations in modules.
    instance TVars TCTopEntity where
      apSubst :: Subst -> TCTopEntity -> TCTopEntity
    apSubst Subst
    su TCTopEntity
    ent =
        case TCTopEntity
    ent of
          TCTopModule ModuleG ModName
    m -> ModuleG ModName -> TCTopEntity
    TCTopModule (Subst -> ModuleG ModName -> ModuleG ModName
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su ModuleG ModName
    m)
          TCTopSignature {} -> TCTopEntity
    ent