-- (c) The University of Glasgow 2006

{-# LANGUAGE ScopedTypeVariables, PatternSynonyms, MultiWayIf #-}

{-# LANGUAGE DeriveFunctor #-}

module GHC.Core.Unify (
        tcMatchTy, tcMatchTyKi,
        tcMatchTys, tcMatchTyKis,
        tcMatchTyX, tcMatchTysX, tcMatchTyKisX,
        tcMatchTyX_BM, ruleMatchTyKiX,

        -- Side-effect free unification
        tcUnifyTy, tcUnifyTyKi, tcUnifyTys, tcUnifyTyKis,
        tcUnifyTysFG, tcUnifyTyWithTFs,
        BindFun, BindFlag(..), matchBindFun, alwaysBindFun,
        UnifyResult, UnifyResultM(..), MaybeApartReason(..),
        typesCantMatch, typesAreApart,

        -- Matching a type against a lifted type (coercion)
        liftCoMatch,

        -- The core flattening algorithm
        flattenTys, flattenTysX,

   ) where

import GHC.Prelude

import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Name( Name, mkSysTvName, mkSystemVarName )
import GHC.Builtin.Names( tYPETyConKey, cONSTRAINTTyConKey )
import GHC.Core.Type     hiding ( getTvSubstEnv )
import GHC.Core.Coercion hiding ( getCvSubstEnv )
import GHC.Core.TyCon
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Compare ( eqType, tcEqType )
import GHC.Core.TyCo.FVs     ( tyCoVarsOfCoList, tyCoFVsOfTypes )
import GHC.Core.TyCo.Subst   ( mkTvSubst, emptyIdSubstEnv )
import GHC.Core.Map.Type
import GHC.Utils.FV( FV, fvVarList )
import GHC.Utils.Misc
import GHC.Data.Pair
import GHC.Utils.Outputable
import GHC.Types.Unique
import GHC.Types.Unique.FM
import GHC.Types.Unique.Set
import GHC.Exts( oneShot )
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import GHC.Data.FastString

import Data.List ( mapAccumL )
import Control.Monad
import qualified Data.Semigroup as S

{-

Unification is much tricker than you might think.

1. The substitution we generate binds the *template type variables*
   which are given to us explicitly.

2. We want to match in the presence of foralls;
        e.g     (forall a. t1) ~ (forall b. t2)

   That is what the RnEnv2 is for; it does the alpha-renaming
   that makes it as if a and b were the same variable.
   Initialising the RnEnv2, so that it can generate a fresh
   binder when necessary, entails knowing the free variables of
   both types.

3. We must be careful not to bind a template type variable to a
   locally bound variable.  E.g.
        (forall a. x) ~ (forall b. b)
   where x is the template type variable.  Then we do not want to
   bind x to a/b!  This is a kind of occurs check.
   The necessary locals accumulate in the RnEnv2.

Note [tcMatchTy vs tcMatchTyKi]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This module offers two variants of matching: with kinds and without.
The TyKi variant takes two types, of potentially different kinds,
and matches them. Along the way, it necessarily also matches their
kinds. The Ty variant instead assumes that the kinds are already
eqType and so skips matching up the kinds.

How do you choose between them?

1. If you know that the kinds of the two types are eqType, use
   the Ty variant. It is more efficient, as it does less work.

2. If the kinds of variables in the template type might mention type families,
   use the Ty variant (and do other work to make sure the kinds
   work out). These pure unification functions do a straightforward
   syntactic unification and do no complex reasoning about type
   families. Note that the types of the variables in instances can indeed
   mention type families, so instance lookup must use the Ty variant.

   (Nothing goes terribly wrong -- no panics -- if there might be type
   families in kinds in the TyKi variant. You just might get match
   failure even though a reducing a type family would lead to success.)

3. Otherwise, if you're sure that the variable kinds do not mention
   type families and you're not already sure that the kind of the template
   equals the kind of the target, then use the TyKi version.
-}

-- | Some unification functions are parameterised by a 'BindFun', which
-- says whether or not to allow a certain unification to take place.
-- A 'BindFun' takes the 'TyVar' involved along with the 'Type' it will
-- potentially be bound to.
--
-- It is possible for the variable to actually be a coercion variable
-- (Note [Matching coercion variables]), but only when one-way matching.
-- In this case, the 'Type' will be a 'CoercionTy'.
type BindFun = TyCoVar -> Type -> BindFlag

-- | @tcMatchTy t1 t2@ produces a substitution (over fvs(t1))
-- @s@ such that @s(t1)@ equals @t2@.
-- The returned substitution might bind coercion variables,
-- if the variable is an argument to a GADT constructor.
--
-- Precondition: typeKind ty1 `eqType` typeKind ty2
--
-- We don't pass in a set of "template variables" to be bound
-- by the match, because tcMatchTy (and similar functions) are
-- always used on top-level types, so we can bind any of the
-- free variables of the LHS.
-- See also Note [tcMatchTy vs tcMatchTyKi]
tcMatchTy :: Type -> Type -> Maybe Subst
tcMatchTy :: Type -> Type -> Maybe Subst
tcMatchTy Type
ty1 Type
ty2 = [Type] -> [Type] -> Maybe Subst
tcMatchTys [Type
ty1] [Type
ty2]

tcMatchTyX_BM :: BindFun -> Subst
              -> Type -> Type -> Maybe Subst
tcMatchTyX_BM :: BindFun -> Subst -> Type -> Type -> Maybe Subst
tcMatchTyX_BM BindFun
bind_me Subst
subst Type
ty1 Type
ty2
  = BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
tc_match_tys_x BindFun
bind_me Bool
False Subst
subst [Type
ty1] [Type
ty2]

-- | Like 'tcMatchTy', but allows the kinds of the types to differ,
-- and thus matches them as well.
-- See also Note [tcMatchTy vs tcMatchTyKi]
tcMatchTyKi :: Type -> Type -> Maybe Subst
tcMatchTyKi :: Type -> Type -> Maybe Subst
tcMatchTyKi Type
ty1 Type
ty2
  = BindFun -> Bool -> [Type] -> [Type] -> Maybe Subst
tc_match_tys BindFun
alwaysBindFun Bool
True [Type
ty1] [Type
ty2]

-- | This is similar to 'tcMatchTy', but extends a substitution
-- See also Note [tcMatchTy vs tcMatchTyKi]
tcMatchTyX :: Subst            -- ^ Substitution to extend
           -> Type                -- ^ Template
           -> Type                -- ^ Target
           -> Maybe Subst
tcMatchTyX :: Subst -> Type -> Type -> Maybe Subst
tcMatchTyX Subst
subst Type
ty1 Type
ty2
  = BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
tc_match_tys_x BindFun
alwaysBindFun Bool
False Subst
subst [Type
ty1] [Type
ty2]

-- | Like 'tcMatchTy' but over a list of types.
-- See also Note [tcMatchTy vs tcMatchTyKi]
tcMatchTys :: [Type]         -- ^ Template
           -> [Type]         -- ^ Target
           -> Maybe Subst    -- ^ One-shot; in principle the template
                             -- variables could be free in the target
tcMatchTys :: [Type] -> [Type] -> Maybe Subst
tcMatchTys [Type]
tys1 [Type]
tys2
  = BindFun -> Bool -> [Type] -> [Type] -> Maybe Subst
tc_match_tys BindFun
alwaysBindFun Bool
False [Type]
tys1 [Type]
tys2

-- | Like 'tcMatchTyKi' but over a list of types.
-- See also Note [tcMatchTy vs tcMatchTyKi]
tcMatchTyKis :: [Type]         -- ^ Template
             -> [Type]         -- ^ Target
             -> Maybe Subst -- ^ One-shot substitution
tcMatchTyKis :: [Type] -> [Type] -> Maybe Subst
tcMatchTyKis [Type]
tys1 [Type]
tys2
  = BindFun -> Bool -> [Type] -> [Type] -> Maybe Subst
tc_match_tys BindFun
alwaysBindFun Bool
True [Type]
tys1 [Type]
tys2

-- | Like 'tcMatchTys', but extending a substitution
-- See also Note [tcMatchTy vs tcMatchTyKi]
tcMatchTysX :: Subst       -- ^ Substitution to extend
            -> [Type]         -- ^ Template
            -> [Type]         -- ^ Target
            -> Maybe Subst -- ^ One-shot substitution
tcMatchTysX :: Subst -> [Type] -> [Type] -> Maybe Subst
tcMatchTysX Subst
subst [Type]
tys1 [Type]
tys2
  = BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
tc_match_tys_x BindFun
alwaysBindFun Bool
False Subst
subst [Type]
tys1 [Type]
tys2

-- | Like 'tcMatchTyKis', but extending a substitution
-- See also Note [tcMatchTy vs tcMatchTyKi]
tcMatchTyKisX :: Subst        -- ^ Substitution to extend
              -> [Type]          -- ^ Template
              -> [Type]          -- ^ Target
              -> Maybe Subst  -- ^ One-shot substitution
tcMatchTyKisX :: Subst -> [Type] -> [Type] -> Maybe Subst
tcMatchTyKisX Subst
subst [Type]
tys1 [Type]
tys2
  = BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
tc_match_tys_x BindFun
alwaysBindFun Bool
True Subst
subst [Type]
tys1 [Type]
tys2

-- | Same as tc_match_tys_x, but starts with an empty substitution
tc_match_tys :: BindFun
             -> Bool          -- ^ match kinds?
             -> [Type]
             -> [Type]
             -> Maybe Subst
tc_match_tys :: BindFun -> Bool -> [Type] -> [Type] -> Maybe Subst
tc_match_tys BindFun
bind_me Bool
match_kis [Type]
tys1 [Type]
tys2
  = BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
tc_match_tys_x BindFun
bind_me Bool
match_kis (InScopeSet -> Subst
mkEmptySubst InScopeSet
in_scope) [Type]
tys1 [Type]
tys2
  where
    in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet ([Type] -> VarSet
tyCoVarsOfTypes [Type]
tys1 VarSet -> VarSet -> VarSet
`unionVarSet` [Type] -> VarSet
tyCoVarsOfTypes [Type]
tys2)

-- | Worker for 'tcMatchTysX' and 'tcMatchTyKisX'
tc_match_tys_x :: BindFun
               -> Bool          -- ^ match kinds?
               -> Subst
               -> [Type]
               -> [Type]
               -> Maybe Subst
tc_match_tys_x :: BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
tc_match_tys_x BindFun
bind_me Bool
match_kis (Subst InScopeSet
in_scope IdSubstEnv
id_env TvSubstEnv
tv_env CvSubstEnv
cv_env) [Type]
tys1 [Type]
tys2
  = case BindFun
-> Bool
-> Bool
-> Bool
-> RnEnv2
-> TvSubstEnv
-> CvSubstEnv
-> [Type]
-> [Type]
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
tc_unify_tys BindFun
bind_me
                      Bool
False  -- Matching, not unifying
                      Bool
False  -- Not an injectivity check
                      Bool
match_kis
                      (InScopeSet -> RnEnv2
mkRnEnv2 InScopeSet
in_scope) TvSubstEnv
tv_env CvSubstEnv
cv_env [Type]
tys1 [Type]
tys2 of
      Unifiable (TvSubstEnv
tv_env', CvSubstEnv
cv_env')
        -> Subst -> Maybe Subst
forall a. a -> Maybe a
Just (Subst -> Maybe Subst) -> Subst -> Maybe Subst
forall a b. (a -> b) -> a -> b
$ InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
id_env TvSubstEnv
tv_env' CvSubstEnv
cv_env'
      UnifyResultM (TvSubstEnv, CvSubstEnv)
_ -> Maybe Subst
forall a. Maybe a
Nothing

-- | This one is called from the expression matcher,
-- which already has a MatchEnv in hand
ruleMatchTyKiX
  :: TyCoVarSet          -- ^ template variables
  -> RnEnv2
  -> TvSubstEnv          -- ^ type substitution to extend
  -> Type                -- ^ Template
  -> Type                -- ^ Target
  -> Maybe TvSubstEnv
ruleMatchTyKiX :: VarSet -> RnEnv2 -> TvSubstEnv -> Type -> Type -> Maybe TvSubstEnv
ruleMatchTyKiX VarSet
tmpl_tvs RnEnv2
rn_env TvSubstEnv
tenv Type
tmpl Type
target
-- See Note [Kind coercions in Unify]
  = case BindFun
-> Bool
-> Bool
-> Bool
-> RnEnv2
-> TvSubstEnv
-> CvSubstEnv
-> [Type]
-> [Type]
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
tc_unify_tys (VarSet -> BindFun
matchBindFun VarSet
tmpl_tvs) Bool
False Bool
False
                      Bool
True -- <-- this means to match the kinds
                      RnEnv2
rn_env TvSubstEnv
tenv CvSubstEnv
emptyCvSubstEnv [Type
tmpl] [Type
target] of
      Unifiable (TvSubstEnv
tenv', CvSubstEnv
_) -> TvSubstEnv -> Maybe TvSubstEnv
forall a. a -> Maybe a
Just TvSubstEnv
tenv'
      UnifyResultM (TvSubstEnv, CvSubstEnv)
_                    -> Maybe TvSubstEnv
forall a. Maybe a
Nothing

-- | Allow binding only for any variable in the set. Variables may
-- be bound to any type.
-- Used when doing simple matching; e.g. can we find a substitution
--
-- @
-- S = [a :-> t1, b :-> t2] such that
--     S( Maybe (a, b->Int )  =   Maybe (Bool, Char -> Int)
-- @
matchBindFun :: TyCoVarSet -> BindFun
matchBindFun :: VarSet -> BindFun
matchBindFun VarSet
tvs OutTyVar
tv Type
_ty
  | OutTyVar
tv OutTyVar -> VarSet -> Bool
`elemVarSet` VarSet
tvs = BindFlag
BindMe
  | Bool
otherwise           = BindFlag
Apart

-- | Allow the binding of any variable to any type
alwaysBindFun :: BindFun
alwaysBindFun :: BindFun
alwaysBindFun OutTyVar
_tv Type
_ty = BindFlag
BindMe

{-
************************************************************************
*                                                                      *
                GADTs
*                                                                      *
************************************************************************

Note [Pruning dead case alternatives]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider        data T a where
                   T1 :: T Int
                   T2 :: T a

                newtype X = MkX Int
                newtype Y = MkY Char

                type family F a
                type instance F Bool = Int

Now consider    case x of { T1 -> e1; T2 -> e2 }

The question before the house is this: if I know something about the type
of x, can I prune away the T1 alternative?

Suppose x::T Char.  It's impossible to construct a (T Char) using T1,
        Answer = YES we can prune the T1 branch (clearly)

Suppose x::T (F a), where 'a' is in scope.  Then 'a' might be instantiated
to 'Bool', in which case x::T Int, so
        ANSWER = NO (clearly)

We see here that we want precisely the apartness check implemented within
tcUnifyTysFG. So that's what we do! Two types cannot match if they are surely
apart. Note that since we are simply dropping dead code, a conservative test
suffices.
-}

-- | Given a list of pairs of types, are any two members of a pair surely
-- apart, even after arbitrary type function evaluation and substitution?
typesCantMatch :: [(Type,Type)] -> Bool
-- See Note [Pruning dead case alternatives]
typesCantMatch :: [(Type, Type)] -> Bool
typesCantMatch [(Type, Type)]
prs = ((Type, Type) -> Bool) -> [(Type, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Type -> Type -> Bool) -> (Type, Type) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Type -> Bool
typesAreApart) [(Type, Type)]
prs

typesAreApart :: Type -> Type -> Bool
typesAreApart :: Type -> Type -> Bool
typesAreApart Type
t1 Type
t2 = case BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTysFG BindFun
alwaysBindFun [Type
t1] [Type
t2] of
                        UnifyResult
SurelyApart -> Bool
True
                        UnifyResult
_           -> Bool
False
{-
************************************************************************
*                                                                      *
             Unification
*                                                                      *
************************************************************************

Note [Fine-grained unification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Do the types (x, x) and ([y], y) unify? The answer is seemingly "no" --
no substitution to finite types makes these match. But, a substitution to
*infinite* types can unify these two types: [x |-> [[[...]]], y |-> [[[...]]] ].
Why do we care? Consider these two type family instances:

type instance F x x   = Int
type instance F [y] y = Bool

If we also have

type instance Looper = [Looper]

then the instances potentially overlap. The solution is to use unification
over infinite terms. This is possible (see [1] for lots of gory details), but
a full algorithm is a little more power than we need. Instead, we make a
conservative approximation and just omit the occurs check.

[1]: http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf

tcUnifyTys considers an occurs-check problem as the same as general unification
failure.

tcUnifyTysFG ("fine-grained") returns one of three results: success, occurs-check
failure ("MaybeApart"), or general failure ("SurelyApart").

See also #8162.

It's worth noting that unification in the presence of infinite types is not
complete. This means that, sometimes, a closed type family does not reduce
when it should. See test case indexed-types/should_fail/Overlap15 for an
example.

Note [Unification result]
~~~~~~~~~~~~~~~~~~~~~~~~~
When unifying t1 ~ t2, we return
* Unifiable s, if s is a substitution such that s(t1) is syntactically the
  same as s(t2), modulo type-synonym expansion.
* SurelyApart, if there is no substitution s such that s(t1) = s(t2),
  where "=" includes type-family reductions.
* MaybeApart mar s, when we aren't sure. `mar` is a MaybeApartReason.

Examples
* [a] ~ Maybe b: SurelyApart, because [] and Maybe can't unify
* [(a,Int)] ~ [(Bool,b)]:  Unifiable
* [F Int] ~ [Bool]: MaybeApart MARTypeFamily, because F Int might reduce to Bool (the unifier
                    does not try this)
* a ~ Maybe a: MaybeApart MARInfinite. Not Unifiable clearly, but not SurelyApart either; consider
       a := Loop
       where  type family Loop where Loop = Maybe Loop

There is the possibility that two types are MaybeApart for *both* reasons:

* (a, F Int) ~ (Maybe a, Bool)

What reason should we use? The *only* consumer of the reason is described
in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv. The goal
there is identify which instances might match a target later (but don't
match now) -- except that we want to ignore the possibility of infinitary
substitutions. So let's examine a concrete scenario:

  class C a b c
  instance C a (Maybe a) Bool
  -- other instances, including one that will actually match
  [W] C b b (F Int)

Do we want the instance as a future possibility? No. The only way that
instance can match is in the presence of an infinite type (infinitely
nested Maybes). We thus say that MARInfinite takes precedence, so that
InstEnv treats this case as an infinitary substitution case; the fact
that a type family is involved is only incidental. We thus define
the Semigroup instance for MaybeApartReason to prefer MARInfinite.

Note [The substitution in MaybeApart]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The constructor MaybeApart carries data with it, typically a TvSubstEnv. Why?
Because consider unifying these:

(a, a, Int) ~ (b, [b], Bool)

If we go left-to-right, we start with [a |-> b]. Then, on the middle terms, we
apply the subst we have so far and discover that we need [b |-> [b]]. Because
this fails the occurs check, we say that the types are MaybeApart (see above
Note [Fine-grained unification]). But, we can't stop there! Because if we
continue, we discover that Int is SurelyApart from Bool, and therefore the
types are apart. This has practical consequences for the ability for closed
type family applications to reduce. See test case
indexed-types/should_compile/Overlap14.

-}

-- | Simple unification of two types; all type variables are bindable
-- Precondition: the kinds are already equal
tcUnifyTy :: Type -> Type       -- All tyvars are bindable
          -> Maybe Subst
                       -- A regular one-shot (idempotent) substitution
tcUnifyTy :: Type -> Type -> Maybe Subst
tcUnifyTy Type
t1 Type
t2 = BindFun -> [Type] -> [Type] -> Maybe Subst
tcUnifyTys BindFun
alwaysBindFun [Type
t1] [Type
t2]

-- | Like 'tcUnifyTy', but also unifies the kinds
tcUnifyTyKi :: Type -> Type -> Maybe Subst
tcUnifyTyKi :: Type -> Type -> Maybe Subst
tcUnifyTyKi Type
t1 Type
t2 = BindFun -> [Type] -> [Type] -> Maybe Subst
tcUnifyTyKis BindFun
alwaysBindFun [Type
t1] [Type
t2]

-- | Unify two types, treating type family applications as possibly unifying
-- with anything and looking through injective type family applications.
-- Precondition: kinds are the same
tcUnifyTyWithTFs :: Bool  -- ^ True <=> do two-way unification;
                          --   False <=> do one-way matching.
                          --   See end of sec 5.2 from the paper
                 -> InScopeSet     -- Should include the free tyvars of both Type args
                 -> Type -> Type   -- Types to unify
                 -> Maybe Subst
-- This algorithm is an implementation of the "Algorithm U" presented in
-- the paper "Injective type families for Haskell", Figures 2 and 3.
-- The code is incorporated with the standard unifier for convenience, but
-- its operation should match the specification in the paper.
tcUnifyTyWithTFs :: Bool -> InScopeSet -> Type -> Type -> Maybe Subst
tcUnifyTyWithTFs Bool
twoWay InScopeSet
in_scope Type
t1 Type
t2
  = case BindFun
-> Bool
-> Bool
-> Bool
-> RnEnv2
-> TvSubstEnv
-> CvSubstEnv
-> [Type]
-> [Type]
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
tc_unify_tys BindFun
alwaysBindFun Bool
twoWay Bool
True Bool
False
                       RnEnv2
rn_env TvSubstEnv
emptyTvSubstEnv CvSubstEnv
emptyCvSubstEnv
                       [Type
t1] [Type
t2] of
      Unifiable          (TvSubstEnv
tv_subst, CvSubstEnv
_cv_subst) -> Subst -> Maybe Subst
forall a. a -> Maybe a
Just (Subst -> Maybe Subst) -> Subst -> Maybe Subst
forall a b. (a -> b) -> a -> b
$ TvSubstEnv -> Subst
maybe_fix TvSubstEnv
tv_subst
      MaybeApart MaybeApartReason
_reason (TvSubstEnv
tv_subst, CvSubstEnv
_cv_subst) -> Subst -> Maybe Subst
forall a. a -> Maybe a
Just (Subst -> Maybe Subst) -> Subst -> Maybe Subst
forall a b. (a -> b) -> a -> b
$ TvSubstEnv -> Subst
maybe_fix TvSubstEnv
tv_subst
      -- we want to *succeed* in questionable cases. This is a
      -- pre-unification algorithm.
      UnifyResultM (TvSubstEnv, CvSubstEnv)
SurelyApart      -> Maybe Subst
forall a. Maybe a
Nothing
  where
    rn_env :: RnEnv2
rn_env   = InScopeSet -> RnEnv2
mkRnEnv2 InScopeSet
in_scope

    maybe_fix :: TvSubstEnv -> Subst
maybe_fix | Bool
twoWay    = InScopeSet -> TvSubstEnv -> Subst
niFixSubst InScopeSet
in_scope
              | Bool
otherwise = InScopeSet -> TvSubstEnv -> Subst
mkTvSubst InScopeSet
in_scope -- when matching, don't confuse
                                               -- domain with range

-----------------
tcUnifyTys :: BindFun
           -> [Type] -> [Type]
           -> Maybe Subst
                                -- ^ A regular one-shot (idempotent) substitution
                                -- that unifies the erased types. See comments
                                -- for 'tcUnifyTysFG'

-- The two types may have common type variables, and indeed do so in the
-- second call to tcUnifyTys in GHC.Tc.Instance.FunDeps.checkClsFD
tcUnifyTys :: BindFun -> [Type] -> [Type] -> Maybe Subst
tcUnifyTys BindFun
bind_fn [Type]
tys1 [Type]
tys2
  = case BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTysFG BindFun
bind_fn [Type]
tys1 [Type]
tys2 of
      Unifiable Subst
result -> Subst -> Maybe Subst
forall a. a -> Maybe a
Just Subst
result
      UnifyResult
_                -> Maybe Subst
forall a. Maybe a
Nothing

-- | Like 'tcUnifyTys' but also unifies the kinds
tcUnifyTyKis :: BindFun
             -> [Type] -> [Type]
             -> Maybe Subst
tcUnifyTyKis :: BindFun -> [Type] -> [Type] -> Maybe Subst
tcUnifyTyKis BindFun
bind_fn [Type]
tys1 [Type]
tys2
  = case BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTyKisFG BindFun
bind_fn [Type]
tys1 [Type]
tys2 of
      Unifiable Subst
result -> Subst -> Maybe Subst
forall a. a -> Maybe a
Just Subst
result
      UnifyResult
_                -> Maybe Subst
forall a. Maybe a
Nothing

-- This type does double-duty. It is used in the UM (unifier monad) and to
-- return the final result. See Note [Fine-grained unification]
type UnifyResult = UnifyResultM Subst

-- | See Note [Unification result]
data UnifyResultM a = Unifiable a        -- the subst that unifies the types
                    | MaybeApart MaybeApartReason
                                 a       -- the subst has as much as we know
                                         -- it must be part of a most general unifier
                                         -- See Note [The substitution in MaybeApart]
                    | SurelyApart
                    deriving (forall a b. (a -> b) -> UnifyResultM a -> UnifyResultM b)
-> (forall a b. a -> UnifyResultM b -> UnifyResultM a)
-> Functor UnifyResultM
forall a b. a -> UnifyResultM b -> UnifyResultM a
forall a b. (a -> b) -> UnifyResultM a -> UnifyResultM 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) -> UnifyResultM a -> UnifyResultM b
fmap :: forall a b. (a -> b) -> UnifyResultM a -> UnifyResultM b
$c<$ :: forall a b. a -> UnifyResultM b -> UnifyResultM a
<$ :: forall a b. a -> UnifyResultM b -> UnifyResultM a
Functor

-- | Why are two types 'MaybeApart'? 'MARInfinite' takes precedence:
-- This is used (only) in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv
-- As of Feb 2022, we never differentiate between MARTypeFamily and MARTypeVsConstraint;
-- it's really only MARInfinite that's interesting here.
data MaybeApartReason
  = MARTypeFamily   -- ^ matching e.g. F Int ~? Bool

  | MARInfinite     -- ^ matching e.g. a ~? Maybe a

  | MARTypeVsConstraint  -- ^ matching Type ~? Constraint or the arrow types
    -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim

instance Outputable MaybeApartReason where
  ppr :: MaybeApartReason -> SDoc
ppr MaybeApartReason
MARTypeFamily       = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"MARTypeFamily"
  ppr MaybeApartReason
MARInfinite         = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"MARInfinite"
  ppr MaybeApartReason
MARTypeVsConstraint = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"MARTypeVsConstraint"

instance Semigroup MaybeApartReason where
  -- see end of Note [Unification result] for why
  MaybeApartReason
MARTypeFamily       <> :: MaybeApartReason -> MaybeApartReason -> MaybeApartReason
<> MaybeApartReason
r = MaybeApartReason
r
  MaybeApartReason
MARInfinite         <> MaybeApartReason
_ = MaybeApartReason
MARInfinite
  MaybeApartReason
MARTypeVsConstraint <> MaybeApartReason
r = MaybeApartReason
r

instance Applicative UnifyResultM where
  pure :: forall a. a -> UnifyResultM a
pure  = a -> UnifyResultM a
forall a. a -> UnifyResultM a
Unifiable
  <*> :: forall a b.
UnifyResultM (a -> b) -> UnifyResultM a -> UnifyResultM b
(<*>) = UnifyResultM (a -> b) -> UnifyResultM a -> UnifyResultM b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad UnifyResultM where
  UnifyResultM a
SurelyApart  >>= :: forall a b.
UnifyResultM a -> (a -> UnifyResultM b) -> UnifyResultM b
>>= a -> UnifyResultM b
_ = UnifyResultM b
forall a. UnifyResultM a
SurelyApart
  MaybeApart MaybeApartReason
r1 a
x >>= a -> UnifyResultM b
f = case a -> UnifyResultM b
f a
x of
                            Unifiable b
y     -> MaybeApartReason -> b -> UnifyResultM b
forall a. MaybeApartReason -> a -> UnifyResultM a
MaybeApart MaybeApartReason
r1 b
y
                            MaybeApart MaybeApartReason
r2 b
y -> MaybeApartReason -> b -> UnifyResultM b
forall a. MaybeApartReason -> a -> UnifyResultM a
MaybeApart (MaybeApartReason
r1 MaybeApartReason -> MaybeApartReason -> MaybeApartReason
forall a. Semigroup a => a -> a -> a
S.<> MaybeApartReason
r2) b
y
                            UnifyResultM b
SurelyApart     -> UnifyResultM b
forall a. UnifyResultM a
SurelyApart
  Unifiable a
x  >>= a -> UnifyResultM b
f = a -> UnifyResultM b
f a
x

-- | @tcUnifyTysFG bind_tv tys1 tys2@ attempts to find a substitution @s@ (whose
-- domain elements all respond 'BindMe' to @bind_tv@) such that
-- @s(tys1)@ and that of @s(tys2)@ are equal, as witnessed by the returned
-- Coercions. This version requires that the kinds of the types are the same,
-- if you unify left-to-right.
tcUnifyTysFG :: BindFun
             -> [Type] -> [Type]
             -> UnifyResult
tcUnifyTysFG :: BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTysFG BindFun
bind_fn [Type]
tys1 [Type]
tys2
  = Bool -> BindFun -> [Type] -> [Type] -> UnifyResult
tc_unify_tys_fg Bool
False BindFun
bind_fn [Type]
tys1 [Type]
tys2

tcUnifyTyKisFG :: BindFun
               -> [Type] -> [Type]
               -> UnifyResult
tcUnifyTyKisFG :: BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTyKisFG BindFun
bind_fn [Type]
tys1 [Type]
tys2
  = Bool -> BindFun -> [Type] -> [Type] -> UnifyResult
tc_unify_tys_fg Bool
True BindFun
bind_fn [Type]
tys1 [Type]
tys2

tc_unify_tys_fg :: Bool
                -> BindFun
                -> [Type] -> [Type]
                -> UnifyResult
tc_unify_tys_fg :: Bool -> BindFun -> [Type] -> [Type] -> UnifyResult
tc_unify_tys_fg Bool
match_kis BindFun
bind_fn [Type]
tys1 [Type]
tys2
  = do { (TvSubstEnv
env, CvSubstEnv
_) <- BindFun
-> Bool
-> Bool
-> Bool
-> RnEnv2
-> TvSubstEnv
-> CvSubstEnv
-> [Type]
-> [Type]
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
tc_unify_tys BindFun
bind_fn Bool
True Bool
False Bool
match_kis RnEnv2
rn_env
                                  TvSubstEnv
emptyTvSubstEnv CvSubstEnv
emptyCvSubstEnv
                                  [Type]
tys1 [Type]
tys2
       ; Subst -> UnifyResult
forall a. a -> UnifyResultM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> UnifyResult) -> Subst -> UnifyResult
forall a b. (a -> b) -> a -> b
$ InScopeSet -> TvSubstEnv -> Subst
niFixSubst InScopeSet
in_scope TvSubstEnv
env }
  where
    in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [Type] -> VarSet
tyCoVarsOfTypes [Type]
tys1 VarSet -> VarSet -> VarSet
`unionVarSet` [Type] -> VarSet
tyCoVarsOfTypes [Type]
tys2
    rn_env :: RnEnv2
rn_env   = InScopeSet -> RnEnv2
mkRnEnv2 InScopeSet
in_scope

-- | This function is actually the one to call the unifier -- a little
-- too general for outside clients, though.
tc_unify_tys :: BindFun
             -> AmIUnifying -- ^ True <=> unify; False <=> match
             -> Bool        -- ^ True <=> doing an injectivity check
             -> Bool        -- ^ True <=> treat the kinds as well
             -> RnEnv2
             -> TvSubstEnv  -- ^ substitution to extend
             -> CvSubstEnv
             -> [Type] -> [Type]
             -> UnifyResultM (TvSubstEnv, CvSubstEnv)
-- NB: It's tempting to ASSERT here that, if we're not matching kinds, then
-- the kinds of the types should be the same. However, this doesn't work,
-- as the types may be a dependent telescope, where later types have kinds
-- that mention variables occurring earlier in the list of types. Here's an
-- example (from typecheck/should_fail/T12709):
--   template: [rep :: RuntimeRep,       a :: TYPE rep]
--   target:   [LiftedRep :: RuntimeRep, Int :: TYPE LiftedRep]
-- We can see that matching the first pair will make the kinds of the second
-- pair equal. Yet, we still don't need a separate pass to unify the kinds
-- of these types, so it's appropriate to use the Ty variant of unification.
-- See also Note [tcMatchTy vs tcMatchTyKi].
tc_unify_tys :: BindFun
-> Bool
-> Bool
-> Bool
-> RnEnv2
-> TvSubstEnv
-> CvSubstEnv
-> [Type]
-> [Type]
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
tc_unify_tys BindFun
bind_fn Bool
unif Bool
inj_check Bool
match_kis RnEnv2
rn_env TvSubstEnv
tv_env CvSubstEnv
cv_env [Type]
tys1 [Type]
tys2
  = TvSubstEnv
-> CvSubstEnv
-> UM (TvSubstEnv, CvSubstEnv)
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
forall a. TvSubstEnv -> CvSubstEnv -> UM a -> UnifyResultM a
initUM TvSubstEnv
tv_env CvSubstEnv
cv_env (UM (TvSubstEnv, CvSubstEnv)
 -> UnifyResultM (TvSubstEnv, CvSubstEnv))
-> UM (TvSubstEnv, CvSubstEnv)
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
forall a b. (a -> b) -> a -> b
$
    do { Bool -> UM () -> UM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
match_kis (UM () -> UM ()) -> UM () -> UM ()
forall a b. (a -> b) -> a -> b
$
         UMEnv -> [Type] -> [Type] -> UM ()
unify_tys UMEnv
env [Type]
kis1 [Type]
kis2
       ; UMEnv -> [Type] -> [Type] -> UM ()
unify_tys UMEnv
env [Type]
tys1 [Type]
tys2
       ; (,) (TvSubstEnv -> CvSubstEnv -> (TvSubstEnv, CvSubstEnv))
-> UM TvSubstEnv -> UM (CvSubstEnv -> (TvSubstEnv, CvSubstEnv))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UM TvSubstEnv
getTvSubstEnv UM (CvSubstEnv -> (TvSubstEnv, CvSubstEnv))
-> UM CvSubstEnv -> UM (TvSubstEnv, CvSubstEnv)
forall a b. UM (a -> b) -> UM a -> UM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UM CvSubstEnv
getCvSubstEnv }
  where
    env :: UMEnv
env = UMEnv { um_bind_fun :: BindFun
um_bind_fun = BindFun
bind_fn
                , um_skols :: VarSet
um_skols    = VarSet
emptyVarSet
                , um_unif :: Bool
um_unif     = Bool
unif
                , um_inj_tf :: Bool
um_inj_tf   = Bool
inj_check
                , um_rn_env :: RnEnv2
um_rn_env   = RnEnv2
rn_env }

    kis1 :: [Type]
kis1 = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (() :: Constraint) => Type -> Type
Type -> Type
typeKind [Type]
tys1
    kis2 :: [Type]
kis2 = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (() :: Constraint) => Type -> Type
Type -> Type
typeKind [Type]
tys2

instance Outputable a => Outputable (UnifyResultM a) where
  ppr :: UnifyResultM a -> SDoc
ppr UnifyResultM a
SurelyApart      = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"SurelyApart"
  ppr (Unifiable a
x)    = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Unifiable" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
x
  ppr (MaybeApart MaybeApartReason
r a
x) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"MaybeApart" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> MaybeApartReason -> SDoc
forall a. Outputable a => a -> SDoc
ppr MaybeApartReason
r SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
x

{-
************************************************************************
*                                                                      *
                Non-idempotent substitution
*                                                                      *
************************************************************************

Note [Non-idempotent substitution]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
During unification we use a TvSubstEnv/CvSubstEnv pair that is
  (a) non-idempotent
  (b) loop-free; ie repeatedly applying it yields a fixed point

Note [Finding the substitution fixpoint]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Finding the fixpoint of a non-idempotent substitution arising from a
unification is much trickier than it looks, because of kinds.  Consider
   T k (H k (f:k)) ~ T * (g:*)
If we unify, we get the substitution
   [ k -> *
   , g -> H k (f:k) ]
To make it idempotent we don't want to get just
   [ k -> *
   , g -> H * (f:k) ]
We also want to substitute inside f's kind, to get
   [ k -> *
   , g -> H k (f:*) ]
If we don't do this, we may apply the substitution to something,
and get an ill-formed type, i.e. one where typeKind will fail.
This happened, for example, in #9106.

It gets worse.  In #14164 we wanted to take the fixpoint of
this substitution
   [ xs_asV :-> F a_aY6 (z_aY7 :: a_aY6)
                        (rest_aWF :: G a_aY6 (z_aY7 :: a_aY6))
   , a_aY6  :-> a_aXQ ]

We have to apply the substitution for a_aY6 two levels deep inside
the invocation of F!  We don't have a function that recursively
applies substitutions inside the kinds of variable occurrences (and
probably rightly so).

So, we work as follows:

 1. Start with the current substitution (which we are
    trying to fixpoint
       [ xs :-> F a (z :: a) (rest :: G a (z :: a))
       , a  :-> b ]

 2. Take all the free vars of the range of the substitution:
       {a, z, rest, b}
    NB: the free variable finder closes over
    the kinds of variable occurrences

 3. If none are in the domain of the substitution, stop.
    We have found a fixpoint.

 4. Remove the variables that are bound by the substitution, leaving
       {z, rest, b}

 5. Do a topo-sort to put them in dependency order:
       [ b :: *, z :: a, rest :: G a z ]

 6. Apply the substitution left-to-right to the kinds of these
    tyvars, extending it each time with a new binding, so we
    finish up with
       [ xs   :-> ..as before..
       , a    :-> b
       , b    :-> b    :: *
       , z    :-> z    :: b
       , rest :-> rest :: G b (z :: b) ]
    Note that rest now has the right kind

 7. Apply this extended substitution (once) to the range of
    the /original/ substitution.  (Note that we do the
    extended substitution would go on forever if you tried
    to find its fixpoint, because it maps z to z.)

 8. And go back to step 1

In Step 6 we use the free vars from Step 2 as the initial
in-scope set, because all of those variables appear in the
range of the substitution, so they must all be in the in-scope
set.  But NB that the type substitution engine does not look up
variables in the in-scope set; it is used only to ensure no
shadowing.
-}

niFixSubst :: InScopeSet -> TvSubstEnv -> Subst
-- Find the idempotent fixed point of the non-idempotent substitution
-- This is surprisingly tricky:
--   see Note [Finding the substitution fixpoint]
-- ToDo: use laziness instead of iteration?
niFixSubst :: InScopeSet -> TvSubstEnv -> Subst
niFixSubst InScopeSet
in_scope TvSubstEnv
tenv
  | Bool
not_fixpoint = InScopeSet -> TvSubstEnv -> Subst
niFixSubst InScopeSet
in_scope ((Type -> Type) -> TvSubstEnv -> TvSubstEnv
forall a b. (a -> b) -> VarEnv a -> VarEnv b
mapVarEnv ((() :: Constraint) => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst) TvSubstEnv
tenv)
  | Bool
otherwise    = Subst
subst
  where
    range_fvs :: FV
    range_fvs :: FV
range_fvs = [Type] -> FV
tyCoFVsOfTypes (TvSubstEnv -> [Type]
forall key elt. UniqFM key elt -> [elt]
nonDetEltsUFM TvSubstEnv
tenv)
          -- It's OK to use nonDetEltsUFM here because the
          -- order of range_fvs, range_tvs is immaterial

    range_tvs :: [TyVar]
    range_tvs :: [OutTyVar]
range_tvs = FV -> [OutTyVar]
fvVarList FV
range_fvs

    not_fixpoint :: Bool
not_fixpoint  = (OutTyVar -> Bool) -> [OutTyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any OutTyVar -> Bool
in_domain [OutTyVar]
range_tvs
    in_domain :: OutTyVar -> Bool
in_domain OutTyVar
tv  = OutTyVar
tv OutTyVar -> TvSubstEnv -> Bool
forall a. OutTyVar -> VarEnv a -> Bool
`elemVarEnv` TvSubstEnv
tenv

    free_tvs :: [OutTyVar]
free_tvs = [OutTyVar] -> [OutTyVar]
scopedSort ((OutTyVar -> Bool) -> [OutTyVar] -> [OutTyVar]
forall a. (a -> Bool) -> [a] -> [a]
filterOut OutTyVar -> Bool
in_domain [OutTyVar]
range_tvs)

    -- See Note [Finding the substitution fixpoint], Step 6
    subst :: Subst
subst = (Subst -> OutTyVar -> Subst) -> Subst -> [OutTyVar] -> Subst
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Subst -> OutTyVar -> Subst
add_free_tv
                  (InScopeSet -> TvSubstEnv -> Subst
mkTvSubst InScopeSet
in_scope TvSubstEnv
tenv)
                  [OutTyVar]
free_tvs

    add_free_tv :: Subst -> TyVar -> Subst
    add_free_tv :: Subst -> OutTyVar -> Subst
add_free_tv Subst
subst OutTyVar
tv
      = Subst -> OutTyVar -> Type -> Subst
extendTvSubst Subst
subst OutTyVar
tv (OutTyVar -> Type
mkTyVarTy OutTyVar
tv')
     where
        tv' :: OutTyVar
tv' = (Type -> Type) -> OutTyVar -> OutTyVar
updateTyVarKind ((() :: Constraint) => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst) OutTyVar
tv

niSubstTvSet :: TvSubstEnv -> TyCoVarSet -> TyCoVarSet
-- Apply the non-idempotent substitution to a set of type variables,
-- remembering that the substitution isn't necessarily idempotent
-- This is used in the occurs check, before extending the substitution
niSubstTvSet :: TvSubstEnv -> VarSet -> VarSet
niSubstTvSet TvSubstEnv
tsubst VarSet
tvs
  = (OutTyVar -> VarSet -> VarSet) -> VarSet -> VarSet -> VarSet
forall elt a. (elt -> a -> a) -> a -> UniqSet elt -> a
nonDetStrictFoldUniqSet (VarSet -> VarSet -> VarSet
unionVarSet (VarSet -> VarSet -> VarSet)
-> (OutTyVar -> VarSet) -> OutTyVar -> VarSet -> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutTyVar -> VarSet
get) VarSet
emptyVarSet VarSet
tvs
  -- It's OK to use a non-deterministic fold here because we immediately forget
  -- the ordering by creating a set.
  where
    get :: OutTyVar -> VarSet
get OutTyVar
tv
      | Just Type
ty <- TvSubstEnv -> OutTyVar -> Maybe Type
forall a. VarEnv a -> OutTyVar -> Maybe a
lookupVarEnv TvSubstEnv
tsubst OutTyVar
tv
      = TvSubstEnv -> VarSet -> VarSet
niSubstTvSet TvSubstEnv
tsubst (Type -> VarSet
tyCoVarsOfType Type
ty)

      | Bool
otherwise
      = OutTyVar -> VarSet
unitVarSet OutTyVar
tv

{-
************************************************************************
*                                                                      *
                unify_ty: the main workhorse
*                                                                      *
************************************************************************

Note [Specification of unification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The pure unifier, unify_ty, defined in this module, tries to work out
a substitution to make two types say True to eqType. NB: eqType is
itself not purely syntactic; it accounts for CastTys;
see Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep

Unlike the "impure unifiers" in the typechecker (the eager unifier in
GHC.Tc.Utils.Unify, and the constraint solver itself in GHC.Tc.Solver.Canonical), the pure
unifier does /not/ work up to ~.

The algorithm implemented here is rather delicate, and we depend on it
to uphold certain properties. This is a summary of these required
properties.

Notation:
 θ,φ  substitutions
 ξ    type-function-free types
 τ,σ  other types
 τ♭   type τ, flattened

 ≡    eqType

(U1) Soundness.
     If (unify τ₁ τ₂) = Unifiable θ, then θ(τ₁) ≡ θ(τ₂).
     θ is a most general unifier for τ₁ and τ₂.

(U2) Completeness.
     If (unify ξ₁ ξ₂) = SurelyApart,
     then there exists no substitution θ such that θ(ξ₁) ≡ θ(ξ₂).

These two properties are stated as Property 11 in the "Closed Type Families"
paper (POPL'14). Below, this paper is called [CTF].

(U3) Apartness under substitution.
     If (unify ξ τ♭) = SurelyApart, then (unify ξ θ(τ)♭) = SurelyApart,
     for any θ. (Property 12 from [CTF])

(U4) Apart types do not unify.
     If (unify ξ τ♭) = SurelyApart, then there exists no θ
     such that θ(ξ) = θ(τ). (Property 13 from [CTF])

THEOREM. Completeness w.r.t ~
    If (unify τ₁♭ τ₂♭) = SurelyApart,
    then there exists no proof that (τ₁ ~ τ₂).

PROOF. See appendix of [CTF].


The unification algorithm is used for type family injectivity, as described
in the "Injective Type Families" paper (Haskell'15), called [ITF]. When run
in this mode, it has the following properties.

(I1) If (unify σ τ) = SurelyApart, then σ and τ are not unifiable, even
     after arbitrary type family reductions. Note that σ and τ are
     not flattened here.

(I2) If (unify σ τ) = MaybeApart θ, and if some
     φ exists such that φ(σ) ~ φ(τ), then φ extends θ.


Furthermore, the RULES matching algorithm requires this property,
but only when using this algorithm for matching:

(M1) If (match σ τ) succeeds with θ, then all matchable tyvars
     in σ are bound in θ.

     Property M1 means that we must extend the substitution with,
     say (a ↦ a) when appropriate during matching.
     See also Note [Self-substitution when matching].

(M2) Completeness of matching.
     If θ(σ) = τ, then (match σ τ) = Unifiable φ,
     where θ is an extension of φ.

Sadly, property M2 and I2 conflict. Consider

type family F1 a b where
  F1 Int    Bool   = Char
  F1 Double String = Char

Consider now two matching problems:

P1. match (F1 a Bool) (F1 Int Bool)
P2. match (F1 a Bool) (F1 Double String)

In case P1, we must find (a ↦ Int) to satisfy M2.
In case P2, we must /not/ find (a ↦ Double), in order to satisfy I2. (Note
that the correct mapping for I2 is (a ↦ Int). There is no way to discover
this, but we mustn't map a to anything else!)

We thus must parameterize the algorithm over whether it's being used
for an injectivity check (refrain from looking at non-injective arguments
to type families) or not (do indeed look at those arguments).  This is
implemented  by the um_inj_tf field of UMEnv.

(It's all a question of whether or not to include equation (7) from Fig. 2
of [ITF].)

This extra parameter is a bit fiddly, perhaps, but seemingly less so than
having two separate, almost-identical algorithms.

Note [Self-substitution when matching]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
What should happen when we're *matching* (not unifying) a1 with a1? We
should get a substitution [a1 |-> a1]. A successful match should map all
the template variables (except ones that disappear when expanding synonyms).
But when unifying, we don't want to do this, because we'll then fall into
a loop.

This arrangement affects the code in three places:
 - If we're matching a refined template variable, don't recur. Instead, just
   check for equality. That is, if we know [a |-> Maybe a] and are matching
   (a ~? Maybe Int), we want to just fail.

 - Skip the occurs check when matching. This comes up in two places, because
   matching against variables is handled separately from matching against
   full-on types.

Note that this arrangement was provoked by a real failure, where the same
unique ended up in the template as in the target. (It was a rule firing when
compiling Data.List.NonEmpty.)

Note [Matching coercion variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:

   type family F a

   data G a where
     MkG :: F a ~ Bool => G a

   type family Foo (x :: G a) :: F a
   type instance Foo MkG = False

We would like that to be accepted. For that to work, we need to introduce
a coercion variable on the left and then use it on the right. Accordingly,
at use sites of Foo, we need to be able to use matching to figure out the
value for the coercion. (See the desugared version:

   axFoo :: [a :: *, c :: F a ~ Bool]. Foo (MkG c) = False |> (sym c)

) We never want this action to happen during *unification* though, when
all bets are off.

Note [Kind coercions in Unify]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We wish to match/unify while ignoring casts. But, we can't just ignore
them completely, or we'll end up with ill-kinded substitutions. For example,
say we're matching `a` with `ty |> co`. If we just drop the cast, we'll
return [a |-> ty], but `a` and `ty` might have different kinds. We can't
just match/unify their kinds, either, because this might gratuitously
fail. After all, `co` is the witness that the kinds are the same -- they
may look nothing alike.

So, we pass a kind coercion to the match/unify worker. This coercion witnesses
the equality between the substed kind of the left-hand type and the substed
kind of the right-hand type. Note that we do not unify kinds at the leaves
(as we did previously). We thus have

Hence: (Unification Kind Invariant)
-----------------------------------
In the call
     unify_ty ty1 ty2 kco
it must be that
     subst(kco) :: subst(kind(ty1)) ~N subst(kind(ty2))
where `subst` is the ambient substitution in the UM monad.  And in the call
     unify_tys tys1 tys2
(which has no kco), after we unify any prefix of tys1,tys2, the kinds of the
head of the remaining tys1,tys2 are identical after substitution.  This
implies, for example, that the kinds of the head of tys1,tys2 are identical
after substitution.

To get this coercion, we first have to match/unify
the kinds before looking at the types. Happily, we need look only one level
up, as all kinds are guaranteed to have kind *.

When we're working with type applications (either TyConApp or AppTy) we
need to worry about establishing INVARIANT, as the kinds of the function
& arguments aren't (necessarily) included in the kind of the result.
When unifying two TyConApps, this is easy, because the two TyCons are
the same. Their kinds are thus the same. As long as we unify left-to-right,
we'll be sure to unify types' kinds before the types themselves. (For example,
think about Proxy :: forall k. k -> *. Unifying the first args matches up
the kinds of the second args.)

For AppTy, we must unify the kinds of the functions, but once these are
unified, we can continue unifying arguments without worrying further about
kinds.

The interface to this module includes both "...Ty" functions and
"...TyKi" functions. The former assume that INVARIANT is already
established, either because the kinds are the same or because the
list of types being passed in are the well-typed arguments to some
type constructor (see two paragraphs above). The latter take a separate
pre-pass over the kinds to establish INVARIANT. Sometimes, it's important
not to take the second pass, as it caused #12442.

We thought, at one point, that this was all unnecessary: why should
casts be in types in the first place? But they are sometimes. In
dependent/should_compile/KindEqualities2, we see, for example the
constraint Num (Int |> (blah ; sym blah)).  We naturally want to find
a dictionary for that constraint, which requires dealing with
coercions in this manner.

Note [Matching in the presence of casts (1)]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When matching, it is crucial that no variables from the template
end up in the range of the matching substitution (obviously!).
When unifying, that's not a constraint; instead we take the fixpoint
of the substitution at the end.

So what should we do with this, when matching?
   unify_ty (tmpl |> co) tgt kco

Previously, wrongly, we pushed 'co' in the (horrid) accumulating
'kco' argument like this:
   unify_ty (tmpl |> co) tgt kco
     = unify_ty tmpl tgt (kco ; co)

But that is obviously wrong because 'co' (from the template) ends
up in 'kco', which in turn ends up in the range of the substitution.

This all came up in #13910.  Because we match tycon arguments
left-to-right, the ambient substitution will already have a matching
substitution for any kinds; so there is an easy fix: just apply
the substitution-so-far to the coercion from the LHS.

Note that

* When matching, the first arg of unify_ty is always the template;
  we never swap round.

* The above argument is distressingly indirect. We seek a
  better way.

* One better way is to ensure that type patterns (the template
  in the matching process) have no casts.  See #14119.

Note [Matching in the presence of casts (2)]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
There is another wrinkle (#17395).  Suppose (T :: forall k. k -> Type)
and we are matching
   tcMatchTy (T k (a::k))  (T j (b::j))

Then we'll match k :-> j, as expected. But then in unify_tys
we invoke
   unify_tys env (a::k) (b::j) (Refl j)

Although we have unified k and j, it's very important that we put
(Refl j), /not/ (Refl k) as the fourth argument to unify_tys.
If we put (Refl k) we'd end up with the substitution
  a :-> b |> Refl k
which is bogus because one of the template variables, k,
appears in the range of the substitution.  Eek.

Similar care is needed in unify_ty_app.


Note [Polykinded tycon applications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose  T :: forall k. Type -> K
and we are unifying
  ty1:  T @Type         Int       :: Type
  ty2:  T @(Type->Type) Int Int   :: Type

These two TyConApps have the same TyCon at the front but they
(legitimately) have different numbers of arguments.  They
are surelyApart, so we can report that without looking any
further (see #15704).

Note [Unifying type applications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Unifying type applications is quite subtle, as we found
in #23134 and #22647, when type families are involved.

Suppose
   type family F a :: Type -> Type
   type family G k :: k = r | r -> k

and consider these examples:

* F Int ~ F Char, where F is injective
  Since F is injective, we can reduce this to Int ~ Char,
  therefore SurelyApart.

* F Int ~ F Char, where F is not injective
  Without injectivity, return MaybeApart.

* G Type ~ G (Type -> Type) Int
  Even though G is injective and the arguments to G are different,
  we cannot deduce apartness because the RHS is oversaturated.
  For example, G might be defined as
    G Type = Maybe Int
    G (Type -> Type) = Maybe
  So we return MaybeApart.

* F Int Bool ~ F Int Char       -- SurelyApart (since Bool is apart from Char)
  F Int Bool ~ Maybe a          -- MaybeApart
  F Int Bool ~ a b              -- MaybeApart
  F Int Bool ~ Char -> Bool     -- MaybeApart
  An oversaturated type family can match an application,
  whether it's a TyConApp, AppTy or FunTy. Decompose.

* F Int ~ a b
  We cannot decompose a saturated, or under-saturated
  type family application. We return MaybeApart.

To handle all those conditions, unify_ty goes through
the following checks in sequence, where Fn is a type family
of arity n:

* (C1) Fn x_1 ... x_n ~ Fn y_1 .. y_n
  A saturated application.
  Here we can unify arguments in which Fn is injective.
* (C2) Fn x_1 ... x_n ~ anything, anything ~ Fn x_1 ... x_n
  A saturated type family can match anything - we return MaybeApart.
* (C3) Fn x_1 ... x_m ~ a b, a b ~ Fn x_1 ... x_m where m > n
  An oversaturated type family can be decomposed.
* (C4) Fn x_1 ... x_m ~ anything, anything ~ Fn x_1 ... x_m, where m > n
  If we couldn't decompose in the previous step, we return SurelyApart.

Afterwards, the rest of the code doesn't have to worry about type families.
-}

-------------- unify_ty: the main workhorse -----------

type AmIUnifying = Bool   -- True  <=> Unifying
                          -- False <=> Matching

unify_ty :: UMEnv
         -> Type -> Type  -- Types to be unified and a co
         -> CoercionN     -- A coercion between their kinds
                          -- See Note [Kind coercions in Unify]
         -> UM ()
-- Precondition: see (Unification Kind Invariant)
--
-- See Note [Specification of unification]
-- Respects newtypes, PredTypes
-- See Note [Computing equality on types] in GHC.Core.Type
unify_ty :: UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
_env (TyConApp TyCon
tc1 []) (TyConApp TyCon
tc2 []) CoercionN
_kco
  -- See Note [Comparing nullary type synonyms] in GHC.Core.Type.
  | TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
  = () -> UM ()
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

unify_ty UMEnv
env Type
ty1 Type
ty2 CoercionN
kco
    -- Now handle the cases we can "look through": synonyms and casts.
  | Just Type
ty1' <- Type -> Maybe Type
coreView Type
ty1 = UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
ty1' Type
ty2 CoercionN
kco
  | Just Type
ty2' <- Type -> Maybe Type
coreView Type
ty2 = UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
ty1 Type
ty2' CoercionN
kco
  | CastTy Type
ty1' CoercionN
co <- Type
ty1     = if UMEnv -> Bool
um_unif UMEnv
env
                                then UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
ty1' Type
ty2 (CoercionN
co CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN
kco)
                                else -- See Note [Matching in the presence of casts (1)]
                                     do { Subst
subst <- UMEnv -> UM Subst
getSubst UMEnv
env
                                        ; let co' :: CoercionN
co' = (() :: Constraint) => Subst -> CoercionN -> CoercionN
Subst -> CoercionN -> CoercionN
substCo Subst
subst CoercionN
co
                                        ; UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
ty1' Type
ty2 (CoercionN
co' CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN
kco) }
  | CastTy Type
ty2' CoercionN
co <- Type
ty2     = UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
ty1 Type
ty2' (CoercionN
kco CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN -> CoercionN
mkSymCo CoercionN
co)

unify_ty UMEnv
env (TyVarTy OutTyVar
tv1) Type
ty2 CoercionN
kco
  = UMEnv -> OutTyVar -> Type -> CoercionN -> UM ()
uVar UMEnv
env OutTyVar
tv1 Type
ty2 CoercionN
kco
unify_ty UMEnv
env Type
ty1 (TyVarTy OutTyVar
tv2) CoercionN
kco
  | UMEnv -> Bool
um_unif UMEnv
env  -- If unifying, can swap args
  = UMEnv -> OutTyVar -> Type -> CoercionN -> UM ()
uVar (UMEnv -> UMEnv
umSwapRn UMEnv
env) OutTyVar
tv2 Type
ty1 (CoercionN -> CoercionN
mkSymCo CoercionN
kco)

unify_ty UMEnv
env Type
ty1 Type
ty2 CoercionN
_kco

  -- Handle non-oversaturated type families first
  -- See Note [Unifying type applications]
  --
  -- (C1) If we have T x1 ... xn ~ T y1 ... yn, use injectivity information of T
  -- Note that both sides must not be oversaturated
  | Just (TyCon
tc1, [Type]
tys1) <- Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
isSatTyFamApp Maybe (TyCon, [Type])
mb_tc_app1
  , Just (TyCon
tc2, [Type]
tys2) <- Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
isSatTyFamApp Maybe (TyCon, [Type])
mb_tc_app2
  , TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
  = do { let inj :: [Bool]
inj = case TyCon -> Injectivity
tyConInjectivityInfo TyCon
tc1 of
                          Injectivity
NotInjective -> Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False
                          Injective [Bool]
bs -> [Bool]
bs

             ([Type]
inj_tys1, [Type]
noninj_tys1) = [Bool] -> [Type] -> ([Type], [Type])
forall a. [Bool] -> [a] -> ([a], [a])
partitionByList [Bool]
inj [Type]
tys1
             ([Type]
inj_tys2, [Type]
noninj_tys2) = [Bool] -> [Type] -> ([Type], [Type])
forall a. [Bool] -> [a] -> ([a], [a])
partitionByList [Bool]
inj [Type]
tys2

       ; UMEnv -> [Type] -> [Type] -> UM ()
unify_tys UMEnv
env [Type]
inj_tys1 [Type]
inj_tys2
       ; Bool -> UM () -> UM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (UMEnv -> Bool
um_inj_tf UMEnv
env) (UM () -> UM ()) -> UM () -> UM ()
forall a b. (a -> b) -> a -> b
$ -- See (end of) Note [Specification of unification]
         MaybeApartReason -> UM () -> UM ()
don'tBeSoSure MaybeApartReason
MARTypeFamily (UM () -> UM ()) -> UM () -> UM ()
forall a b. (a -> b) -> a -> b
$ UMEnv -> [Type] -> [Type] -> UM ()
unify_tys UMEnv
env [Type]
noninj_tys1 [Type]
noninj_tys2 }

  | Just (TyCon, [Type])
_ <- Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
isSatTyFamApp Maybe (TyCon, [Type])
mb_tc_app1  -- (C2) A (not-over-saturated) type-family application
  = MaybeApartReason -> UM ()
maybeApart MaybeApartReason
MARTypeFamily            -- behaves like a type variable; might match

  | Just (TyCon, [Type])
_ <- Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
isSatTyFamApp Maybe (TyCon, [Type])
mb_tc_app2  -- (C2) A (not-over-saturated) type-family application
                                        -- behaves like a type variable; might unify
                                        -- but doesn't match (as in the TyVarTy case)
  = if UMEnv -> Bool
um_unif UMEnv
env then MaybeApartReason -> UM ()
maybeApart MaybeApartReason
MARTypeFamily else UM ()
forall a. UM a
surelyApart

  -- Handle oversaturated type families.
  --
  -- They can match an application (TyConApp/FunTy/AppTy), this is handled
  -- the same way as in the AppTy case below.
  --
  -- If there is no application, an oversaturated type family can only
  -- match a type variable or a saturated type family,
  -- both of which we handled earlier. So we can say surelyApart.
  | Just (TyCon
tc1, [Type]
_) <- Maybe (TyCon, [Type])
mb_tc_app1
  , TyCon -> Bool
isTypeFamilyTyCon TyCon
tc1
  = if | Just (Type
ty1a, Type
ty1b) <- Type -> Maybe (Type, Type)
tcSplitAppTyNoView_maybe Type
ty1
       , Just (Type
ty2a, Type
ty2b) <- Type -> Maybe (Type, Type)
tcSplitAppTyNoView_maybe Type
ty2
       -> UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app UMEnv
env Type
ty1a [Type
ty1b] Type
ty2a [Type
ty2b]            -- (C3)
       | Bool
otherwise -> UM ()
forall a. UM a
surelyApart                             -- (C4)

  | Just (TyCon
tc2, [Type]
_) <- Maybe (TyCon, [Type])
mb_tc_app2
  , TyCon -> Bool
isTypeFamilyTyCon TyCon
tc2
  = if | Just (Type
ty1a, Type
ty1b) <- Type -> Maybe (Type, Type)
tcSplitAppTyNoView_maybe Type
ty1
       , Just (Type
ty2a, Type
ty2b) <- Type -> Maybe (Type, Type)
tcSplitAppTyNoView_maybe Type
ty2
       -> UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app UMEnv
env Type
ty1a [Type
ty1b] Type
ty2a [Type
ty2b]            -- (C3)
       | Bool
otherwise -> UM ()
forall a. UM a
surelyApart                             -- (C4)

  -- At this point, neither tc1 nor tc2 can be a type family.
  | Just (TyCon
tc1, [Type]
tys1) <- Maybe (TyCon, [Type])
mb_tc_app1
  , Just (TyCon
tc2, [Type]
tys2) <- Maybe (TyCon, [Type])
mb_tc_app2
  , TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
  = do { Bool -> SDoc -> UM ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Bool -> SDoc -> m ()
massertPpr (TyCon -> Role -> Bool
isInjectiveTyCon TyCon
tc1 Role
Nominal) (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc1)
       ; UMEnv -> [Type] -> [Type] -> UM ()
unify_tys UMEnv
env [Type]
tys1 [Type]
tys2
       }

  -- TYPE and CONSTRAINT are not Apart
  -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
  -- NB: at this point we know that the two TyCons do not match
  | Just (TyCon
tc1,[Type]
_) <- Maybe (TyCon, [Type])
mb_tc_app1, let u1 :: Unique
u1 = TyCon -> Unique
tyConUnique TyCon
tc1
  , Just (TyCon
tc2,[Type]
_) <- Maybe (TyCon, [Type])
mb_tc_app2, let u2 :: Unique
u2 = TyCon -> Unique
tyConUnique TyCon
tc2
  , (Unique
u1 Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
tYPETyConKey Bool -> Bool -> Bool
&& Unique
u2 Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
cONSTRAINTTyConKey) Bool -> Bool -> Bool
||
    (Unique
u2 Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
tYPETyConKey Bool -> Bool -> Bool
&& Unique
u1 Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
cONSTRAINTTyConKey)
  = MaybeApartReason -> UM ()
maybeApart MaybeApartReason
MARTypeVsConstraint
    -- We don't bother to look inside; wrinkle (W3) in GHC.Builtin.Types.Prim
    -- Note [Type and Constraint are not apart]

  -- The arrow types are not Apart
  -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
  --     wrinkle (W2)
  -- NB1: at this point we know that the two TyCons do not match
  -- NB2: In the common FunTy/FunTy case you might wonder if we want to go via
  --      splitTyConApp_maybe.  But yes we do: we need to look at those implied
  --      kind argument in order to satisfy (Unification Kind Invariant)
  | FunTy {} <- Type
ty1
  , FunTy {} <- Type
ty2
  = MaybeApartReason -> UM ()
maybeApart MaybeApartReason
MARTypeVsConstraint
    -- We don't bother to look inside; wrinkle (W3) in GHC.Builtin.Types.Prim
    -- Note [Type and Constraint are not apart]

  where
    mb_tc_app1 :: Maybe (TyCon, [Type])
mb_tc_app1 = (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty1
    mb_tc_app2 :: Maybe (TyCon, [Type])
mb_tc_app2 = (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty2

        -- Applications need a bit of care!
        -- They can match FunTy and TyConApp, so use splitAppTy_maybe
        -- NB: we've already dealt with type variables,
        -- so if one type is an App the other one jolly well better be too
unify_ty UMEnv
env (AppTy Type
ty1a Type
ty1b) Type
ty2 CoercionN
_kco
  | Just (Type
ty2a, Type
ty2b) <- Type -> Maybe (Type, Type)
tcSplitAppTyNoView_maybe Type
ty2
  = UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app UMEnv
env Type
ty1a [Type
ty1b] Type
ty2a [Type
ty2b]

unify_ty UMEnv
env Type
ty1 (AppTy Type
ty2a Type
ty2b) CoercionN
_kco
  | Just (Type
ty1a, Type
ty1b) <- Type -> Maybe (Type, Type)
tcSplitAppTyNoView_maybe Type
ty1
  = UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app UMEnv
env Type
ty1a [Type
ty1b] Type
ty2a [Type
ty2b]

unify_ty UMEnv
_ (LitTy TyLit
x) (LitTy TyLit
y) CoercionN
_kco | TyLit
x TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
y = () -> UM ()
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

unify_ty UMEnv
env (ForAllTy (Bndr OutTyVar
tv1 ForAllTyFlag
_) Type
ty1) (ForAllTy (Bndr OutTyVar
tv2 ForAllTyFlag
_) Type
ty2) CoercionN
kco
  = do { UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env (OutTyVar -> Type
varType OutTyVar
tv1) (OutTyVar -> Type
varType OutTyVar
tv2) (Type -> CoercionN
mkNomReflCo Type
liftedTypeKind)
       ; let env' :: UMEnv
env' = UMEnv -> OutTyVar -> OutTyVar -> UMEnv
umRnBndr2 UMEnv
env OutTyVar
tv1 OutTyVar
tv2
       ; UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env' Type
ty1 Type
ty2 CoercionN
kco }

-- See Note [Matching coercion variables]
unify_ty UMEnv
env (CoercionTy CoercionN
co1) (CoercionTy CoercionN
co2) CoercionN
kco
  = do { CvSubstEnv
c_subst <- UM CvSubstEnv
getCvSubstEnv
       ; case CoercionN
co1 of
           CoVarCo OutTyVar
cv
             | Bool -> Bool
not (UMEnv -> Bool
um_unif UMEnv
env)
             , Bool -> Bool
not (OutTyVar
cv OutTyVar -> CvSubstEnv -> Bool
forall a. OutTyVar -> VarEnv a -> Bool
`elemVarEnv` CvSubstEnv
c_subst)
             , let (CoercionN
_, CoercionN
co_l, CoercionN
co_r) = (() :: Constraint) =>
CoercionN -> (CoercionN, CoercionN, CoercionN)
CoercionN -> (CoercionN, CoercionN, CoercionN)
decomposeFunCo CoercionN
kco
                     -- Because the coercion is used in a type, it should be safe to
                     -- ignore the multiplicity coercion.
                      -- cv :: t1 ~ t2
                      -- co2 :: s1 ~ s2
                      -- co_l :: t1 ~ s1
                      -- co_r :: t2 ~ s2
                   rhs_co :: CoercionN
rhs_co = CoercionN
co_l CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN
co2 CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN -> CoercionN
mkSymCo CoercionN
co_r
             , BindFlag
BindMe <- UMEnv -> BindFun
tvBindFlag UMEnv
env OutTyVar
cv (CoercionN -> Type
CoercionTy CoercionN
rhs_co)
             -> do { UMEnv -> VarSet -> UM ()
checkRnEnv UMEnv
env (CoercionN -> VarSet
tyCoVarsOfCo CoercionN
co2)
                   ; OutTyVar -> CoercionN -> UM ()
extendCvEnv OutTyVar
cv CoercionN
rhs_co }
           CoercionN
_ -> () -> UM ()
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return () }

unify_ty UMEnv
_ Type
_ Type
_ CoercionN
_ = UM ()
forall a. UM a
surelyApart

unify_ty_app :: UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app :: UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app UMEnv
env Type
ty1 [Type]
ty1args Type
ty2 [Type]
ty2args
  | Just (Type
ty1', Type
ty1a) <- (() :: Constraint) => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
splitAppTyNoView_maybe Type
ty1
  , Just (Type
ty2', Type
ty2a) <- (() :: Constraint) => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
splitAppTyNoView_maybe Type
ty2
  = UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app UMEnv
env Type
ty1' (Type
ty1a Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ty1args) Type
ty2' (Type
ty2a Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ty2args)

  | Bool
otherwise
  = do { let ki1 :: Type
ki1 = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty1
             ki2 :: Type
ki2 = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty2
           -- See Note [Kind coercions in Unify]
       ; UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty  UMEnv
env Type
ki1 Type
ki2 (Type -> CoercionN
mkNomReflCo Type
liftedTypeKind)
       ; UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty  UMEnv
env Type
ty1 Type
ty2 (Type -> CoercionN
mkNomReflCo Type
ki2)
                 -- Very important: 'ki2' not 'ki1'
                 -- See Note [Matching in the presence of casts (2)]
       ; UMEnv -> [Type] -> [Type] -> UM ()
unify_tys UMEnv
env [Type]
ty1args [Type]
ty2args }

unify_tys :: UMEnv -> [Type] -> [Type] -> UM ()
-- Precondition: see (Unification Kind Invariant)
unify_tys :: UMEnv -> [Type] -> [Type] -> UM ()
unify_tys UMEnv
env [Type]
orig_xs [Type]
orig_ys
  = [Type] -> [Type] -> UM ()
go [Type]
orig_xs [Type]
orig_ys
  where
    go :: [Type] -> [Type] -> UM ()
go []     []     = () -> UM ()
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    go (Type
x:[Type]
xs) (Type
y:[Type]
ys)
      -- See Note [Kind coercions in Unify]
      = do { UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
x Type
y (Type -> CoercionN
mkNomReflCo (Type -> CoercionN) -> Type -> CoercionN
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
y)
                 -- Very important: 'y' not 'x'
                 -- See Note [Matching in the presence of casts (2)]
           ; [Type] -> [Type] -> UM ()
go [Type]
xs [Type]
ys }
    go [Type]
_ [Type]
_ = UM ()
forall a. UM a
surelyApart
      -- Possibly different saturations of a polykinded tycon
      -- See Note [Polykinded tycon applications]

isSatTyFamApp :: Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
-- Return the argument if we have a saturated type family application
-- If it is /over/ saturated then we return False.  E.g.
--     unify_ty (F a b) (c d)    where F has arity 1
-- we definitely want to decompose that type application! (#22647)
isSatTyFamApp :: Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
isSatTyFamApp tapp :: Maybe (TyCon, [Type])
tapp@(Just (TyCon
tc, [Type]
tys))
  |  TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
  Bool -> Bool -> Bool
&& Bool -> Bool
not ([Type]
tys [Type] -> Arity -> Bool
forall a. [a] -> Arity -> Bool
`lengthExceeds` TyCon -> Arity
tyConArity TyCon
tc)  -- Not over-saturated
  = Maybe (TyCon, [Type])
tapp
isSatTyFamApp Maybe (TyCon, [Type])
_ = Maybe (TyCon, [Type])
forall a. Maybe a
Nothing

---------------------------------
uVar :: UMEnv
     -> InTyVar         -- Variable to be unified
     -> Type            -- with this Type
     -> Coercion        -- :: kind tv ~N kind ty
     -> UM ()

uVar :: UMEnv -> OutTyVar -> Type -> CoercionN -> UM ()
uVar UMEnv
env OutTyVar
tv1 Type
ty CoercionN
kco
 = do { -- Apply the ambient renaming
        let tv1' :: OutTyVar
tv1' = UMEnv -> OutTyVar -> OutTyVar
umRnOccL UMEnv
env OutTyVar
tv1

        -- Check to see whether tv1 is refined by the substitution
      ; TvSubstEnv
subst <- UM TvSubstEnv
getTvSubstEnv
      ; case (TvSubstEnv -> OutTyVar -> Maybe Type
forall a. VarEnv a -> OutTyVar -> Maybe a
lookupVarEnv TvSubstEnv
subst OutTyVar
tv1') of
          Just Type
ty' | UMEnv -> Bool
um_unif UMEnv
env                -- Unifying, so call
                   -> UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
ty' Type
ty CoercionN
kco   -- back into unify
                   | Bool
otherwise
                   -> -- Matching, we don't want to just recur here.
                      -- this is because the range of the subst is the target
                      -- type, not the template type. So, just check for
                      -- normal type equality.
                      Bool -> UM () -> UM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((Type
ty' Type -> CoercionN -> Type
`mkCastTy` CoercionN
kco) (() :: Constraint) => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
ty) (UM () -> UM ()) -> UM () -> UM ()
forall a b. (a -> b) -> a -> b
$
                        UM ()
forall a. UM a
surelyApart
                      -- NB: it's important to use `tcEqType` instead of `eqType` here,
                      -- otherwise we might not reject a substitution
                      -- which unifies `Type` with `Constraint`, e.g.
                      -- a call to tc_unify_tys with arguments
                      --
                      --   tys1 = [k,k]
                      --   tys2 = [Type, Constraint]
                      --
                      -- See test cases: T11715b, T20521.
          Maybe Type
Nothing  -> UMEnv -> OutTyVar -> Type -> Type -> CoercionN -> UM ()
uUnrefined UMEnv
env OutTyVar
tv1' Type
ty Type
ty CoercionN
kco } -- No, continue

uUnrefined :: UMEnv
           -> OutTyVar          -- variable to be unified
           -> Type              -- with this Type
           -> Type              -- (version w/ expanded synonyms)
           -> Coercion          -- :: kind tv ~N kind ty
           -> UM ()

-- We know that tv1 isn't refined

uUnrefined :: UMEnv -> OutTyVar -> Type -> Type -> CoercionN -> UM ()
uUnrefined UMEnv
env OutTyVar
tv1' Type
ty2 Type
ty2' CoercionN
kco
  | Just Type
ty2'' <- Type -> Maybe Type
coreView Type
ty2'
  = UMEnv -> OutTyVar -> Type -> Type -> CoercionN -> UM ()
uUnrefined UMEnv
env OutTyVar
tv1' Type
ty2 Type
ty2'' CoercionN
kco    -- Unwrap synonyms
                -- This is essential, in case we have
                --      type Foo a = a
                -- and then unify a ~ Foo a

  | TyVarTy OutTyVar
tv2 <- Type
ty2'
  = do { let tv2' :: OutTyVar
tv2' = UMEnv -> OutTyVar -> OutTyVar
umRnOccR UMEnv
env OutTyVar
tv2
       ; Bool -> UM () -> UM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (OutTyVar
tv1' OutTyVar -> OutTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== OutTyVar
tv2' Bool -> Bool -> Bool
&& UMEnv -> Bool
um_unif UMEnv
env) (UM () -> UM ()) -> UM () -> UM ()
forall a b. (a -> b) -> a -> b
$ do
           -- If we are unifying a ~ a, just return immediately
           -- Do not extend the substitution
           -- See Note [Self-substitution when matching]

          -- Check to see whether tv2 is refined
       { TvSubstEnv
subst <- UM TvSubstEnv
getTvSubstEnv
       ; case TvSubstEnv -> OutTyVar -> Maybe Type
forall a. VarEnv a -> OutTyVar -> Maybe a
lookupVarEnv TvSubstEnv
subst OutTyVar
tv2 of
         {  Just Type
ty' | UMEnv -> Bool
um_unif UMEnv
env -> UMEnv -> OutTyVar -> Type -> Type -> CoercionN -> UM ()
uUnrefined UMEnv
env OutTyVar
tv1' Type
ty' Type
ty' CoercionN
kco
         ;  Maybe Type
_ ->

    do {   -- So both are unrefined
           -- Bind one or the other, depending on which is bindable
       ; let rhs1 :: Type
rhs1 = Type
ty2 Type -> CoercionN -> Type
`mkCastTy` CoercionN -> CoercionN
mkSymCo CoercionN
kco
             rhs2 :: Type
rhs2 = Type
ty1 Type -> CoercionN -> Type
`mkCastTy` CoercionN
kco
             b1 :: BindFlag
b1  = UMEnv -> BindFun
tvBindFlag UMEnv
env OutTyVar
tv1' Type
rhs1
             b2 :: BindFlag
b2  = UMEnv -> BindFun
tvBindFlag UMEnv
env OutTyVar
tv2' Type
rhs2
             ty1 :: Type
ty1 = OutTyVar -> Type
mkTyVarTy OutTyVar
tv1'
       ; case (BindFlag
b1, BindFlag
b2) of
           (BindFlag
BindMe, BindFlag
_) -> UMEnv -> OutTyVar -> Type -> UM ()
bindTv UMEnv
env OutTyVar
tv1' Type
rhs1
           (BindFlag
_, BindFlag
BindMe) | UMEnv -> Bool
um_unif UMEnv
env
                       -> UMEnv -> OutTyVar -> Type -> UM ()
bindTv (UMEnv -> UMEnv
umSwapRn UMEnv
env) OutTyVar
tv2 Type
rhs2

           (BindFlag, BindFlag)
_ | OutTyVar
tv1' OutTyVar -> OutTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== OutTyVar
tv2' -> () -> UM ()
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
             -- How could this happen? If we're only matching and if
             -- we're comparing forall-bound variables.

           (BindFlag, BindFlag)
_ -> UM ()
forall a. UM a
surelyApart
  }}}}

uUnrefined UMEnv
env OutTyVar
tv1' Type
ty2 Type
_ CoercionN
kco -- ty2 is not a type variable
  = case UMEnv -> BindFun
tvBindFlag UMEnv
env OutTyVar
tv1' Type
rhs of
      BindFlag
Apart  -> UM ()
forall a. UM a
surelyApart
      BindFlag
BindMe -> UMEnv -> OutTyVar -> Type -> UM ()
bindTv UMEnv
env OutTyVar
tv1' Type
rhs
  where
    rhs :: Type
rhs = Type
ty2 Type -> CoercionN -> Type
`mkCastTy` CoercionN -> CoercionN
mkSymCo CoercionN
kco

bindTv :: UMEnv -> OutTyVar -> Type -> UM ()
-- OK, so we want to extend the substitution with tv := ty
-- But first, we must do a couple of checks
bindTv :: UMEnv -> OutTyVar -> Type -> UM ()
bindTv UMEnv
env OutTyVar
tv1 Type
ty2
  = do  { let free_tvs2 :: VarSet
free_tvs2 = Type -> VarSet
tyCoVarsOfType Type
ty2

        -- Make sure tys mentions no local variables
        -- E.g.  (forall a. b) ~ (forall a. [a])
        -- We should not unify b := [a]!
        ; UMEnv -> VarSet -> UM ()
checkRnEnv UMEnv
env VarSet
free_tvs2

        -- Occurs check, see Note [Fine-grained unification]
        -- Make sure you include 'kco' (which ty2 does) #14846
        ; Bool
occurs <- UMEnv -> OutTyVar -> VarSet -> UM Bool
occursCheck UMEnv
env OutTyVar
tv1 VarSet
free_tvs2

        ; if Bool
occurs then MaybeApartReason -> UM ()
maybeApart MaybeApartReason
MARInfinite
                    else OutTyVar -> Type -> UM ()
extendTvEnv OutTyVar
tv1 Type
ty2 }

occursCheck :: UMEnv -> TyVar -> VarSet -> UM Bool
occursCheck :: UMEnv -> OutTyVar -> VarSet -> UM Bool
occursCheck UMEnv
env OutTyVar
tv VarSet
free_tvs
  | UMEnv -> Bool
um_unif UMEnv
env
  = do { TvSubstEnv
tsubst <- UM TvSubstEnv
getTvSubstEnv
       ; Bool -> UM Bool
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return (OutTyVar
tv OutTyVar -> VarSet -> Bool
`elemVarSet` TvSubstEnv -> VarSet -> VarSet
niSubstTvSet TvSubstEnv
tsubst VarSet
free_tvs) }

  | Bool
otherwise      -- Matching; no occurs check
  = Bool -> UM Bool
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False   -- See Note [Self-substitution when matching]

{-
%************************************************************************
%*                                                                      *
                Binding decisions
*                                                                      *
************************************************************************
-}

data BindFlag
  = BindMe      -- ^ A regular type variable

  | Apart       -- ^ Declare that this type variable is /apart/ from the
                -- type provided. That is, the type variable will never
                -- be instantiated to that type.
                -- See also Note [Binding when looking up instances]
                -- in GHC.Core.InstEnv.
  deriving BindFlag -> BindFlag -> Bool
(BindFlag -> BindFlag -> Bool)
-> (BindFlag -> BindFlag -> Bool) -> Eq BindFlag
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BindFlag -> BindFlag -> Bool
== :: BindFlag -> BindFlag -> Bool
$c/= :: BindFlag -> BindFlag -> Bool
/= :: BindFlag -> BindFlag -> Bool
Eq
-- NB: It would be conceivable to have an analogue to MaybeApart here,
-- but there is not yet a need.

{-
************************************************************************
*                                                                      *
                Unification monad
*                                                                      *
************************************************************************
-}

data UMEnv
  = UMEnv { UMEnv -> Bool
um_unif :: AmIUnifying

          , UMEnv -> Bool
um_inj_tf :: Bool
            -- Checking for injectivity?
            -- See (end of) Note [Specification of unification]

          , UMEnv -> RnEnv2
um_rn_env :: RnEnv2
            -- Renaming InTyVars to OutTyVars; this eliminates
            -- shadowing, and lines up matching foralls on the left
            -- and right

          , UMEnv -> VarSet
um_skols :: TyVarSet
            -- OutTyVars bound by a forall in this unification;
            -- Do not bind these in the substitution!
            -- See the function tvBindFlag

          , UMEnv -> BindFun
um_bind_fun :: BindFun
            -- User-supplied BindFlag function,
            -- for variables not in um_skols
          }

data UMState = UMState
                   { UMState -> TvSubstEnv
um_tv_env   :: TvSubstEnv
                   , UMState -> CvSubstEnv
um_cv_env   :: CvSubstEnv }

newtype UM a
  = UM' { forall a. UM a -> UMState -> UnifyResultM (UMState, a)
unUM :: UMState -> UnifyResultM (UMState, a) }
    -- See Note [The one-shot state monad trick] in GHC.Utils.Monad
  deriving ((forall a b. (a -> b) -> UM a -> UM b)
-> (forall a b. a -> UM b -> UM a) -> Functor UM
forall a b. a -> UM b -> UM a
forall a b. (a -> b) -> UM a -> UM 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) -> UM a -> UM b
fmap :: forall a b. (a -> b) -> UM a -> UM b
$c<$ :: forall a b. a -> UM b -> UM a
<$ :: forall a b. a -> UM b -> UM a
Functor)

pattern UM :: (UMState -> UnifyResultM (UMState, a)) -> UM a
-- See Note [The one-shot state monad trick] in GHC.Utils.Monad
pattern $mUM :: forall {r} {a}.
UM a
-> ((UMState -> UnifyResultM (UMState, a)) -> r)
-> ((# #) -> r)
-> r
$bUM :: forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM m <- UM' m
  where
    UM UMState -> UnifyResultM (UMState, a)
m = (UMState -> UnifyResultM (UMState, a)) -> UM a
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM' ((UMState -> UnifyResultM (UMState, a))
-> UMState -> UnifyResultM (UMState, a)
forall a b. (a -> b) -> a -> b
oneShot UMState -> UnifyResultM (UMState, a)
m)

instance Applicative UM where
      pure :: forall a. a -> UM a
pure a
a = (UMState -> UnifyResultM (UMState, a)) -> UM a
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM (\UMState
s -> (UMState, a) -> UnifyResultM (UMState, a)
forall a. a -> UnifyResultM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UMState
s, a
a))
      <*> :: forall a b. UM (a -> b) -> UM a -> UM b
(<*>)  = UM (a -> b) -> UM a -> UM b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad UM where
  {-# INLINE (>>=) #-}
  -- See Note [INLINE pragmas and (>>)] in GHC.Utils.Monad
  UM a
m >>= :: forall a b. UM a -> (a -> UM b) -> UM b
>>= a -> UM b
k  = (UMState -> UnifyResultM (UMState, b)) -> UM b
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM (\UMState
state ->
                  do { (UMState
state', a
v) <- UM a -> UMState -> UnifyResultM (UMState, a)
forall a. UM a -> UMState -> UnifyResultM (UMState, a)
unUM UM a
m UMState
state
                     ; UM b -> UMState -> UnifyResultM (UMState, b)
forall a. UM a -> UMState -> UnifyResultM (UMState, a)
unUM (a -> UM b
k a
v) UMState
state' })

instance MonadFail UM where
    fail :: forall a. String -> UM a
fail String
_   = (UMState -> UnifyResultM (UMState, a)) -> UM a
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM (\UMState
_ -> UnifyResultM (UMState, a)
forall a. UnifyResultM a
SurelyApart) -- failed pattern match

initUM :: TvSubstEnv  -- subst to extend
       -> CvSubstEnv
       -> UM a -> UnifyResultM a
initUM :: forall a. TvSubstEnv -> CvSubstEnv -> UM a -> UnifyResultM a
initUM TvSubstEnv
subst_env CvSubstEnv
cv_subst_env UM a
um
  = case UM a -> UMState -> UnifyResultM (UMState, a)
forall a. UM a -> UMState -> UnifyResultM (UMState, a)
unUM UM a
um UMState
state of
      Unifiable (UMState
_, a
subst)    -> a -> UnifyResultM a
forall a. a -> UnifyResultM a
Unifiable a
subst
      MaybeApart MaybeApartReason
r (UMState
_, a
subst) -> MaybeApartReason -> a -> UnifyResultM a
forall a. MaybeApartReason -> a -> UnifyResultM a
MaybeApart MaybeApartReason
r a
subst
      UnifyResultM (UMState, a)
SurelyApart             -> UnifyResultM a
forall a. UnifyResultM a
SurelyApart
  where
    state :: UMState
state = UMState { um_tv_env :: TvSubstEnv
um_tv_env = TvSubstEnv
subst_env
                    , um_cv_env :: CvSubstEnv
um_cv_env = CvSubstEnv
cv_subst_env }

tvBindFlag :: UMEnv -> OutTyVar -> Type -> BindFlag
tvBindFlag :: UMEnv -> BindFun
tvBindFlag UMEnv
env OutTyVar
tv Type
rhs
  | OutTyVar
tv OutTyVar -> VarSet -> Bool
`elemVarSet` UMEnv -> VarSet
um_skols UMEnv
env = BindFlag
Apart
  | Bool
otherwise                    = UMEnv -> BindFun
um_bind_fun UMEnv
env OutTyVar
tv Type
rhs

getTvSubstEnv :: UM TvSubstEnv
getTvSubstEnv :: UM TvSubstEnv
getTvSubstEnv = (UMState -> UnifyResultM (UMState, TvSubstEnv)) -> UM TvSubstEnv
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM ((UMState -> UnifyResultM (UMState, TvSubstEnv)) -> UM TvSubstEnv)
-> (UMState -> UnifyResultM (UMState, TvSubstEnv)) -> UM TvSubstEnv
forall a b. (a -> b) -> a -> b
$ \UMState
state -> (UMState, TvSubstEnv) -> UnifyResultM (UMState, TvSubstEnv)
forall a. a -> UnifyResultM a
Unifiable (UMState
state, UMState -> TvSubstEnv
um_tv_env UMState
state)

getCvSubstEnv :: UM CvSubstEnv
getCvSubstEnv :: UM CvSubstEnv
getCvSubstEnv = (UMState -> UnifyResultM (UMState, CvSubstEnv)) -> UM CvSubstEnv
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM ((UMState -> UnifyResultM (UMState, CvSubstEnv)) -> UM CvSubstEnv)
-> (UMState -> UnifyResultM (UMState, CvSubstEnv)) -> UM CvSubstEnv
forall a b. (a -> b) -> a -> b
$ \UMState
state -> (UMState, CvSubstEnv) -> UnifyResultM (UMState, CvSubstEnv)
forall a. a -> UnifyResultM a
Unifiable (UMState
state, UMState -> CvSubstEnv
um_cv_env UMState
state)

getSubst :: UMEnv -> UM Subst
getSubst :: UMEnv -> UM Subst
getSubst UMEnv
env = do { TvSubstEnv
tv_env <- UM TvSubstEnv
getTvSubstEnv
                  ; CvSubstEnv
cv_env <- UM CvSubstEnv
getCvSubstEnv
                  ; let in_scope :: InScopeSet
in_scope = RnEnv2 -> InScopeSet
rnInScopeSet (UMEnv -> RnEnv2
um_rn_env UMEnv
env)
                  ; Subst -> UM Subst
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return (InScopeSet -> TvSubstEnv -> CvSubstEnv -> IdSubstEnv -> Subst
mkSubst InScopeSet
in_scope TvSubstEnv
tv_env CvSubstEnv
cv_env IdSubstEnv
emptyIdSubstEnv) }

extendTvEnv :: TyVar -> Type -> UM ()
extendTvEnv :: OutTyVar -> Type -> UM ()
extendTvEnv OutTyVar
tv Type
ty = (UMState -> UnifyResultM (UMState, ())) -> UM ()
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM ((UMState -> UnifyResultM (UMState, ())) -> UM ())
-> (UMState -> UnifyResultM (UMState, ())) -> UM ()
forall a b. (a -> b) -> a -> b
$ \UMState
state ->
  (UMState, ()) -> UnifyResultM (UMState, ())
forall a. a -> UnifyResultM a
Unifiable (UMState
state { um_tv_env = extendVarEnv (um_tv_env state) tv ty }, ())

extendCvEnv :: CoVar -> Coercion -> UM ()
extendCvEnv :: OutTyVar -> CoercionN -> UM ()
extendCvEnv OutTyVar
cv CoercionN
co = (UMState -> UnifyResultM (UMState, ())) -> UM ()
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM ((UMState -> UnifyResultM (UMState, ())) -> UM ())
-> (UMState -> UnifyResultM (UMState, ())) -> UM ()
forall a b. (a -> b) -> a -> b
$ \UMState
state ->
  (UMState, ()) -> UnifyResultM (UMState, ())
forall a. a -> UnifyResultM a
Unifiable (UMState
state { um_cv_env = extendVarEnv (um_cv_env state) cv co }, ())

umRnBndr2 :: UMEnv -> TyCoVar -> TyCoVar -> UMEnv
umRnBndr2 :: UMEnv -> OutTyVar -> OutTyVar -> UMEnv
umRnBndr2 UMEnv
env OutTyVar
v1 OutTyVar
v2
  = UMEnv
env { um_rn_env = rn_env', um_skols = um_skols env `extendVarSet` v' }
  where
    (RnEnv2
rn_env', OutTyVar
v') = RnEnv2 -> OutTyVar -> OutTyVar -> (RnEnv2, OutTyVar)
rnBndr2_var (UMEnv -> RnEnv2
um_rn_env UMEnv
env) OutTyVar
v1 OutTyVar
v2

checkRnEnv :: UMEnv -> VarSet -> UM ()
checkRnEnv :: UMEnv -> VarSet -> UM ()
checkRnEnv UMEnv
env VarSet
varset
  | VarSet -> Bool
isEmptyVarSet VarSet
skol_vars           = () -> UM ()
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | VarSet
varset VarSet -> VarSet -> Bool
`disjointVarSet` VarSet
skol_vars = () -> UM ()
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise                         = UM ()
forall a. UM a
surelyApart
  where
    skol_vars :: VarSet
skol_vars = UMEnv -> VarSet
um_skols UMEnv
env
    -- NB: That isEmptyVarSet guard is a critical optimization;
    -- it means we don't have to calculate the free vars of
    -- the type, often saving quite a bit of allocation.

-- | Converts any SurelyApart to a MaybeApart
don'tBeSoSure :: MaybeApartReason -> UM () -> UM ()
don'tBeSoSure :: MaybeApartReason -> UM () -> UM ()
don'tBeSoSure MaybeApartReason
r UM ()
um = (UMState -> UnifyResultM (UMState, ())) -> UM ()
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM ((UMState -> UnifyResultM (UMState, ())) -> UM ())
-> (UMState -> UnifyResultM (UMState, ())) -> UM ()
forall a b. (a -> b) -> a -> b
$ \ UMState
state ->
  case UM () -> UMState -> UnifyResultM (UMState, ())
forall a. UM a -> UMState -> UnifyResultM (UMState, a)
unUM UM ()
um UMState
state of
    UnifyResultM (UMState, ())
SurelyApart -> MaybeApartReason -> (UMState, ()) -> UnifyResultM (UMState, ())
forall a. MaybeApartReason -> a -> UnifyResultM a
MaybeApart MaybeApartReason
r (UMState
state, ())
    UnifyResultM (UMState, ())
other       -> UnifyResultM (UMState, ())
other

umRnOccL :: UMEnv -> TyVar -> TyVar
umRnOccL :: UMEnv -> OutTyVar -> OutTyVar
umRnOccL UMEnv
env OutTyVar
v = RnEnv2 -> OutTyVar -> OutTyVar
rnOccL (UMEnv -> RnEnv2
um_rn_env UMEnv
env) OutTyVar
v

umRnOccR :: UMEnv -> TyVar -> TyVar
umRnOccR :: UMEnv -> OutTyVar -> OutTyVar
umRnOccR UMEnv
env OutTyVar
v = RnEnv2 -> OutTyVar -> OutTyVar
rnOccR (UMEnv -> RnEnv2
um_rn_env UMEnv
env) OutTyVar
v

umSwapRn :: UMEnv -> UMEnv
umSwapRn :: UMEnv -> UMEnv
umSwapRn UMEnv
env = UMEnv
env { um_rn_env = rnSwap (um_rn_env env) }

maybeApart :: MaybeApartReason -> UM ()
maybeApart :: MaybeApartReason -> UM ()
maybeApart MaybeApartReason
r = (UMState -> UnifyResultM (UMState, ())) -> UM ()
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM (\UMState
state -> MaybeApartReason -> (UMState, ()) -> UnifyResultM (UMState, ())
forall a. MaybeApartReason -> a -> UnifyResultM a
MaybeApart MaybeApartReason
r (UMState
state, ()))

surelyApart :: UM a
surelyApart :: forall a. UM a
surelyApart = (UMState -> UnifyResultM (UMState, a)) -> UM a
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM (\UMState
_ -> UnifyResultM (UMState, a)
forall a. UnifyResultM a
SurelyApart)

{-
%************************************************************************
%*                                                                      *
            Matching a (lifted) type against a coercion
%*                                                                      *
%************************************************************************

This section defines essentially an inverse to liftCoSubst. It is defined
here to avoid a dependency from Coercion on this module.

-}

data MatchEnv = ME { MatchEnv -> VarSet
me_tmpls :: TyVarSet
                   , MatchEnv -> RnEnv2
me_env   :: RnEnv2 }

-- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'.  In particular, if
--   @liftCoMatch vars ty co == Just s@, then @liftCoSubst s ty == co@,
--   where @==@ there means that the result of 'liftCoSubst' has the same
--   type as the original co; but may be different under the hood.
--   That is, it matches a type against a coercion of the same
--   "shape", and returns a lifting substitution which could have been
--   used to produce the given coercion from the given type.
--   Note that this function is incomplete -- it might return Nothing
--   when there does indeed exist a possible lifting context.
--
-- This function is incomplete in that it doesn't respect the equality
-- in `eqType`. That is, it's possible that this will succeed for t1 and
-- fail for t2, even when t1 `eqType` t2. That's because it depends on
-- there being a very similar structure between the type and the coercion.
-- This incompleteness shouldn't be all that surprising, especially because
-- it depends on the structure of the coercion, which is a silly thing to do.
--
-- The lifting context produced doesn't have to be exacting in the roles
-- of the mappings. This is because any use of the lifting context will
-- also require a desired role. Thus, this algorithm prefers mapping to
-- nominal coercions where it can do so.
liftCoMatch :: TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext
liftCoMatch :: VarSet -> Type -> CoercionN -> Maybe LiftingContext
liftCoMatch VarSet
tmpls Type
ty CoercionN
co
  = do { CvSubstEnv
cenv1 <- MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
forall a. VarEnv a
emptyVarEnv Type
ki CoercionN
ki_co CoercionN
ki_ki_co CoercionN
ki_ki_co
       ; CvSubstEnv
cenv2 <- MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
cenv1       Type
ty CoercionN
co
                              (Type -> CoercionN
mkNomReflCo Type
co_lkind) (Type -> CoercionN
mkNomReflCo Type
co_rkind)
       ; LiftingContext -> Maybe LiftingContext
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> CvSubstEnv -> LiftingContext
LC (InScopeSet -> Subst
mkEmptySubst InScopeSet
in_scope) CvSubstEnv
cenv2) }
  where
    menv :: MatchEnv
menv     = ME { me_tmpls :: VarSet
me_tmpls = VarSet
tmpls, me_env :: RnEnv2
me_env = InScopeSet -> RnEnv2
mkRnEnv2 InScopeSet
in_scope }
    in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (VarSet
tmpls VarSet -> VarSet -> VarSet
`unionVarSet` CoercionN -> VarSet
tyCoVarsOfCo CoercionN
co)
    -- Like tcMatchTy, assume all the interesting variables
    -- in ty are in tmpls

    ki :: Type
ki       = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty
    ki_co :: CoercionN
ki_co    = CoercionN -> CoercionN
promoteCoercion CoercionN
co
    ki_ki_co :: CoercionN
ki_ki_co = Type -> CoercionN
mkNomReflCo Type
liftedTypeKind

    Pair Type
co_lkind Type
co_rkind = CoercionN -> Pair Type
coercionKind CoercionN
ki_co

-- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
ty_co_match :: MatchEnv   -- ^ ambient helpful info
            -> LiftCoEnv  -- ^ incoming subst
            -> Type       -- ^ ty, type to match
            -> Coercion   -- ^ co :: lty ~r rty, coercion to match against
            -> Coercion   -- ^ :: kind(lsubst(ty)) ~N kind(lty)
            -> Coercion   -- ^ :: kind(rsubst(ty)) ~N kind(rty)
            -> Maybe LiftCoEnv
   -- ^ Just env ==> liftCoSubst Nominal env ty == co, modulo roles.
   -- Also: Just env ==> lsubst(ty) == lty and rsubst(ty) == rty,
   -- where lsubst = lcSubstLeft(env) and rsubst = lcSubstRight(env)
ty_co_match :: MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty CoercionN
co CoercionN
lkco CoercionN
rkco
  | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty' CoercionN
co CoercionN
lkco CoercionN
rkco

  -- handle Refl case:
  | Type -> VarSet
tyCoVarsOfType Type
ty VarSet -> CvSubstEnv -> Bool
forall a. VarSet -> VarEnv a -> Bool
`isNotInDomainOf` CvSubstEnv
subst
  , Just (Type
ty', Role
_) <- CoercionN -> Maybe (Type, Role)
isReflCo_maybe CoercionN
co
  , Type
ty Type -> Type -> Bool
`eqType` Type
ty'
    -- Why `eqType` and not `tcEqType`? Because this function is only used
    -- during coercion optimisation, after type-checking has finished.
  = CvSubstEnv -> Maybe CvSubstEnv
forall a. a -> Maybe a
Just CvSubstEnv
subst

  where
    isNotInDomainOf :: VarSet -> VarEnv a -> Bool
    isNotInDomainOf :: forall a. VarSet -> VarEnv a -> Bool
isNotInDomainOf VarSet
set VarEnv a
env
      = (OutTyVar -> Bool) -> VarSet -> Bool
noneSet (\OutTyVar
v -> OutTyVar -> VarEnv a -> Bool
forall a. OutTyVar -> VarEnv a -> Bool
elemVarEnv OutTyVar
v VarEnv a
env) VarSet
set

    noneSet :: (Var -> Bool) -> VarSet -> Bool
    noneSet :: (OutTyVar -> Bool) -> VarSet -> Bool
noneSet OutTyVar -> Bool
f = (OutTyVar -> Bool) -> VarSet -> Bool
allVarSet (Bool -> Bool
not (Bool -> Bool) -> (OutTyVar -> Bool) -> OutTyVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutTyVar -> Bool
f)

ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty CoercionN
co CoercionN
lkco CoercionN
rkco
  | CastTy Type
ty' CoercionN
co' <- Type
ty
     -- See Note [Matching in the presence of casts (1)]
  = let empty_subst :: Subst
empty_subst  = InScopeSet -> Subst
mkEmptySubst (RnEnv2 -> InScopeSet
rnInScopeSet (MatchEnv -> RnEnv2
me_env MatchEnv
menv))
        substed_co_l :: CoercionN
substed_co_l = (() :: Constraint) => Subst -> CoercionN -> CoercionN
Subst -> CoercionN -> CoercionN
substCo (Subst -> CvSubstEnv -> Subst
liftEnvSubstLeft Subst
empty_subst CvSubstEnv
subst)  CoercionN
co'
        substed_co_r :: CoercionN
substed_co_r = (() :: Constraint) => Subst -> CoercionN -> CoercionN
Subst -> CoercionN -> CoercionN
substCo (Subst -> CvSubstEnv -> Subst
liftEnvSubstRight Subst
empty_subst CvSubstEnv
subst) CoercionN
co'
    in
    MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty' CoercionN
co (CoercionN
substed_co_l CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN
lkco)
                                  (CoercionN
substed_co_r CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN
rkco)

  | SymCo CoercionN
co' <- CoercionN
co
  = CvSubstEnv -> CvSubstEnv
swapLiftCoEnv (CvSubstEnv -> CvSubstEnv) -> Maybe CvSubstEnv -> Maybe CvSubstEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv (CvSubstEnv -> CvSubstEnv
swapLiftCoEnv CvSubstEnv
subst) Type
ty CoercionN
co' CoercionN
rkco CoercionN
lkco

  -- Match a type variable against a non-refl coercion
ty_co_match MatchEnv
menv CvSubstEnv
subst (TyVarTy OutTyVar
tv1) CoercionN
co CoercionN
lkco CoercionN
rkco
  | Just CoercionN
co1' <- CvSubstEnv -> OutTyVar -> Maybe CoercionN
forall a. VarEnv a -> OutTyVar -> Maybe a
lookupVarEnv CvSubstEnv
subst OutTyVar
tv1' -- tv1' is already bound to co1
  = if RnEnv2 -> CoercionN -> CoercionN -> Bool
eqCoercionX (RnEnv2 -> RnEnv2
nukeRnEnvL RnEnv2
rn_env) CoercionN
co1' CoercionN
co
    then CvSubstEnv -> Maybe CvSubstEnv
forall a. a -> Maybe a
Just CvSubstEnv
subst
    else Maybe CvSubstEnv
forall a. Maybe a
Nothing       -- no match since tv1 matches two different coercions

  | OutTyVar
tv1' OutTyVar -> VarSet -> Bool
`elemVarSet` MatchEnv -> VarSet
me_tmpls MatchEnv
menv           -- tv1' is a template var
  = if (OutTyVar -> Bool) -> [OutTyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RnEnv2 -> OutTyVar -> Bool
inRnEnvR RnEnv2
rn_env) (CoercionN -> [OutTyVar]
tyCoVarsOfCoList CoercionN
co)
    then Maybe CvSubstEnv
forall a. Maybe a
Nothing      -- occurs check failed
    else CvSubstEnv -> Maybe CvSubstEnv
forall a. a -> Maybe a
Just (CvSubstEnv -> Maybe CvSubstEnv) -> CvSubstEnv -> Maybe CvSubstEnv
forall a b. (a -> b) -> a -> b
$ CvSubstEnv -> OutTyVar -> CoercionN -> CvSubstEnv
forall a. VarEnv a -> OutTyVar -> a -> VarEnv a
extendVarEnv CvSubstEnv
subst OutTyVar
tv1' (CoercionN -> CvSubstEnv) -> CoercionN -> CvSubstEnv
forall a b. (a -> b) -> a -> b
$
                CoercionN -> CoercionN -> CoercionN -> CoercionN
castCoercionKind CoercionN
co (CoercionN -> CoercionN
mkSymCo CoercionN
lkco) (CoercionN -> CoercionN
mkSymCo CoercionN
rkco)

  | Bool
otherwise
  = Maybe CvSubstEnv
forall a. Maybe a
Nothing

  where
    rn_env :: RnEnv2
rn_env = MatchEnv -> RnEnv2
me_env MatchEnv
menv
    tv1' :: OutTyVar
tv1' = RnEnv2 -> OutTyVar -> OutTyVar
rnOccL RnEnv2
rn_env OutTyVar
tv1

  -- just look through SubCo's. We don't really care about roles here.
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty (SubCo CoercionN
co) CoercionN
lkco CoercionN
rkco
  = MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty CoercionN
co CoercionN
lkco CoercionN
rkco

ty_co_match MatchEnv
menv CvSubstEnv
subst (AppTy Type
ty1a Type
ty1b) CoercionN
co CoercionN
_lkco CoercionN
_rkco
  | Just (CoercionN
co2, CoercionN
arg2) <- CoercionN -> Maybe (CoercionN, CoercionN)
splitAppCo_maybe CoercionN
co     -- c.f. Unify.match on AppTy
  = MatchEnv
-> CvSubstEnv
-> Type
-> [Type]
-> CoercionN
-> [CoercionN]
-> Maybe CvSubstEnv
ty_co_match_app MatchEnv
menv CvSubstEnv
subst Type
ty1a [Type
ty1b] CoercionN
co2 [CoercionN
arg2]
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty1 (AppCo CoercionN
co2 CoercionN
arg2) CoercionN
_lkco CoercionN
_rkco
  | Just (Type
ty1a, Type
ty1b) <- (() :: Constraint) => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
splitAppTyNoView_maybe Type
ty1
       -- yes, the one from Type, not TcType; this is for coercion optimization
  = MatchEnv
-> CvSubstEnv
-> Type
-> [Type]
-> CoercionN
-> [CoercionN]
-> Maybe CvSubstEnv
ty_co_match_app MatchEnv
menv CvSubstEnv
subst Type
ty1a [Type
ty1b] CoercionN
co2 [CoercionN
arg2]

ty_co_match MatchEnv
menv CvSubstEnv
subst (TyConApp TyCon
tc1 [Type]
tys) (TyConAppCo Role
_ TyCon
tc2 [CoercionN]
cos) CoercionN
_lkco CoercionN
_rkco
  = MatchEnv
-> CvSubstEnv
-> TyCon
-> [Type]
-> TyCon
-> [CoercionN]
-> Maybe CvSubstEnv
ty_co_match_tc MatchEnv
menv CvSubstEnv
subst TyCon
tc1 [Type]
tys TyCon
tc2 [CoercionN]
cos

ty_co_match MatchEnv
menv CvSubstEnv
subst (FunTy { ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
ty1, ft_res :: Type -> Type
ft_res = Type
ty2 })
            (FunCo { fco_mult :: CoercionN -> CoercionN
fco_mult = CoercionN
co_w, fco_arg :: CoercionN -> CoercionN
fco_arg = CoercionN
co1, fco_res :: CoercionN -> CoercionN
fco_res = CoercionN
co2 }) CoercionN
_lkco CoercionN
_rkco
  = MatchEnv -> CvSubstEnv -> [Type] -> [CoercionN] -> Maybe CvSubstEnv
ty_co_match_args MatchEnv
menv CvSubstEnv
subst [Type
w,    Type
rep1,    Type
rep2,    Type
ty1, Type
ty2]
                                [CoercionN
co_w, CoercionN
co1_rep, CoercionN
co2_rep, CoercionN
co1, CoercionN
co2]
  where
     rep1 :: Type
rep1    = (() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
ty1
     rep2 :: Type
rep2    = (() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
ty2
     co1_rep :: CoercionN
co1_rep = (() :: Constraint) => CoercionN -> CoercionN
CoercionN -> CoercionN
mkRuntimeRepCo CoercionN
co1
     co2_rep :: CoercionN
co2_rep = (() :: Constraint) => CoercionN -> CoercionN
CoercionN -> CoercionN
mkRuntimeRepCo CoercionN
co2
    -- NB: we include the RuntimeRep arguments in the matching;
    --     not doing so caused #21205.

ty_co_match MatchEnv
menv CvSubstEnv
subst (ForAllTy (Bndr OutTyVar
tv1 ForAllTyFlag
_) Type
ty1)
                       (ForAllCo OutTyVar
tv2 CoercionN
kind_co2 CoercionN
co2)
                       CoercionN
lkco CoercionN
rkco
  | OutTyVar -> Bool
isTyVar OutTyVar
tv1 Bool -> Bool -> Bool
&& OutTyVar -> Bool
isTyVar OutTyVar
tv2
  = do { CvSubstEnv
subst1 <- MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst (OutTyVar -> Type
tyVarKind OutTyVar
tv1) CoercionN
kind_co2
                               CoercionN
ki_ki_co CoercionN
ki_ki_co
       ; let rn_env0 :: RnEnv2
rn_env0 = MatchEnv -> RnEnv2
me_env MatchEnv
menv
             rn_env1 :: RnEnv2
rn_env1 = RnEnv2 -> OutTyVar -> OutTyVar -> RnEnv2
rnBndr2 RnEnv2
rn_env0 OutTyVar
tv1 OutTyVar
tv2
             menv' :: MatchEnv
menv'   = MatchEnv
menv { me_env = rn_env1 }
       ; MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv' CvSubstEnv
subst1 Type
ty1 CoercionN
co2 CoercionN
lkco CoercionN
rkco }
  where
    ki_ki_co :: CoercionN
ki_ki_co = Type -> CoercionN
mkNomReflCo Type
liftedTypeKind

-- ty_co_match menv subst (ForAllTy (Bndr cv1 _) ty1)
--                        (ForAllCo cv2 kind_co2 co2)
--                        lkco rkco
--   | isCoVar cv1 && isCoVar cv2
--   We seems not to have enough information for this case
--   1. Given:
--        cv1      :: (s1 :: k1) ~r (s2 :: k2)
--        kind_co2 :: (s1' ~ s2') ~N (t1 ~ t2)
--        eta1      = mkSelCo (SelTyCon 2 role) (downgradeRole r Nominal kind_co2)
--                 :: s1' ~ t1
--        eta2      = mkSelCo (SelTyCon 3 role) (downgradeRole r Nominal kind_co2)
--                 :: s2' ~ t2
--      Wanted:
--        subst1 <- ty_co_match menv subst  s1 eta1 kco1 kco2
--        subst2 <- ty_co_match menv subst1 s2 eta2 kco3 kco4
--      Question: How do we get kcoi?
--   2. Given:
--        lkco :: <*>    -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
--        rkco :: <*>
--      Wanted:
--        ty_co_match menv' subst2 ty1 co2 lkco' rkco'
--      Question: How do we get lkco' and rkco'?

ty_co_match MatchEnv
_ CvSubstEnv
subst (CoercionTy {}) CoercionN
_ CoercionN
_ CoercionN
_
  = CvSubstEnv -> Maybe CvSubstEnv
forall a. a -> Maybe a
Just CvSubstEnv
subst -- don't inspect coercions

ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty (GRefl Role
r Type
t (MCo CoercionN
co)) CoercionN
lkco CoercionN
rkco
  =  MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty (Role -> Type -> MCoercion -> CoercionN
GRefl Role
r Type
t MCoercion
MRefl) CoercionN
lkco (CoercionN
rkco CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN -> CoercionN
mkSymCo CoercionN
co)

ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty CoercionN
co1 CoercionN
lkco CoercionN
rkco
  | Just (CastTy Type
t CoercionN
co, Role
r) <- CoercionN -> Maybe (Type, Role)
isReflCo_maybe CoercionN
co1
  -- In @pushRefl@, pushing reflexive coercion inside CastTy will give us
  -- t |> co ~ t ; <t> ; t ~ t |> co
  -- But transitive coercions are not helpful. Therefore we deal
  -- with it here: we do recursion on the smaller reflexive coercion,
  -- while propagating the correct kind coercions.
  = let kco' :: CoercionN
kco' = CoercionN -> CoercionN
mkSymCo CoercionN
co
    in MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty (Role -> Type -> CoercionN
mkReflCo Role
r Type
t) (CoercionN
lkco CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN
kco')
                                                (CoercionN
rkco CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN
kco')

ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty CoercionN
co CoercionN
lkco CoercionN
rkco
  | Just CoercionN
co' <- CoercionN -> Maybe CoercionN
pushRefl CoercionN
co = MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty CoercionN
co' CoercionN
lkco CoercionN
rkco
  | Bool
otherwise               = Maybe CvSubstEnv
forall a. Maybe a
Nothing

ty_co_match_tc :: MatchEnv -> LiftCoEnv
               -> TyCon -> [Type]
               -> TyCon -> [Coercion]
               -> Maybe LiftCoEnv
ty_co_match_tc :: MatchEnv
-> CvSubstEnv
-> TyCon
-> [Type]
-> TyCon
-> [CoercionN]
-> Maybe CvSubstEnv
ty_co_match_tc MatchEnv
menv CvSubstEnv
subst TyCon
tc1 [Type]
tys1 TyCon
tc2 [CoercionN]
cos2
  = do { Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2)
       ; MatchEnv -> CvSubstEnv -> [Type] -> [CoercionN] -> Maybe CvSubstEnv
ty_co_match_args MatchEnv
menv CvSubstEnv
subst [Type]
tys1 [CoercionN]
cos2 }

ty_co_match_app :: MatchEnv -> LiftCoEnv
                -> Type -> [Type] -> Coercion -> [Coercion]
                -> Maybe LiftCoEnv
ty_co_match_app :: MatchEnv
-> CvSubstEnv
-> Type
-> [Type]
-> CoercionN
-> [CoercionN]
-> Maybe CvSubstEnv
ty_co_match_app MatchEnv
menv CvSubstEnv
subst Type
ty1 [Type]
ty1args CoercionN
co2 [CoercionN]
co2args
  | Just (Type
ty1', Type
ty1a) <- (() :: Constraint) => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
splitAppTyNoView_maybe Type
ty1
  , Just (CoercionN
co2', CoercionN
co2a) <- CoercionN -> Maybe (CoercionN, CoercionN)
splitAppCo_maybe CoercionN
co2
  = MatchEnv
-> CvSubstEnv
-> Type
-> [Type]
-> CoercionN
-> [CoercionN]
-> Maybe CvSubstEnv
ty_co_match_app MatchEnv
menv CvSubstEnv
subst Type
ty1' (Type
ty1a Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ty1args) CoercionN
co2' (CoercionN
co2a CoercionN -> [CoercionN] -> [CoercionN]
forall a. a -> [a] -> [a]
: [CoercionN]
co2args)

  | Bool
otherwise
  = do { CvSubstEnv
subst1 <- MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ki1 CoercionN
ki2 CoercionN
ki_ki_co CoercionN
ki_ki_co
       ; let Pair CoercionN
lkco CoercionN
rkco = Type -> CoercionN
mkNomReflCo (Type -> CoercionN) -> Pair Type -> Pair CoercionN
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoercionN -> Pair Type
coercionKind CoercionN
ki2
       ; CvSubstEnv
subst2 <- MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst1 Type
ty1 CoercionN
co2 CoercionN
lkco CoercionN
rkco
       ; MatchEnv -> CvSubstEnv -> [Type] -> [CoercionN] -> Maybe CvSubstEnv
ty_co_match_args MatchEnv
menv CvSubstEnv
subst2 [Type]
ty1args [CoercionN]
co2args }
  where
    ki1 :: Type
ki1 = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty1
    ki2 :: CoercionN
ki2 = CoercionN -> CoercionN
promoteCoercion CoercionN
co2
    ki_ki_co :: CoercionN
ki_ki_co = Type -> CoercionN
mkNomReflCo Type
liftedTypeKind

ty_co_match_args :: MatchEnv -> LiftCoEnv -> [Type] -> [Coercion]
                 -> Maybe LiftCoEnv
ty_co_match_args :: MatchEnv -> CvSubstEnv -> [Type] -> [CoercionN] -> Maybe CvSubstEnv
ty_co_match_args MatchEnv
menv CvSubstEnv
subst (Type
ty:[Type]
tys) (CoercionN
arg:[CoercionN]
args)
  = do { let Pair Type
lty Type
rty = CoercionN -> Pair Type
coercionKind CoercionN
arg
             lkco :: CoercionN
lkco = Type -> CoercionN
mkNomReflCo ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
lty)
             rkco :: CoercionN
rkco = Type -> CoercionN
mkNomReflCo ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
rty)
       ; CvSubstEnv
subst' <- MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty CoercionN
arg CoercionN
lkco CoercionN
rkco
       ; MatchEnv -> CvSubstEnv -> [Type] -> [CoercionN] -> Maybe CvSubstEnv
ty_co_match_args MatchEnv
menv CvSubstEnv
subst' [Type]
tys [CoercionN]
args }
ty_co_match_args MatchEnv
_    CvSubstEnv
subst []       [] = CvSubstEnv -> Maybe CvSubstEnv
forall a. a -> Maybe a
Just CvSubstEnv
subst
ty_co_match_args MatchEnv
_    CvSubstEnv
_     [Type]
_        [CoercionN]
_  = Maybe CvSubstEnv
forall a. Maybe a
Nothing

pushRefl :: Coercion -> Maybe Coercion
pushRefl :: CoercionN -> Maybe CoercionN
pushRefl CoercionN
co =
  case (CoercionN -> Maybe (Type, Role)
isReflCo_maybe CoercionN
co) of
    Just (AppTy Type
ty1 Type
ty2, Role
Nominal)
      -> CoercionN -> Maybe CoercionN
forall a. a -> Maybe a
Just (CoercionN -> CoercionN -> CoercionN
AppCo (Role -> Type -> CoercionN
mkReflCo Role
Nominal Type
ty1) (Type -> CoercionN
mkNomReflCo Type
ty2))
    Just (FunTy FunTyFlag
af Type
w Type
ty1 Type
ty2, Role
r)
      ->  CoercionN -> Maybe CoercionN
forall a. a -> Maybe a
Just (Role
-> FunTyFlag
-> FunTyFlag
-> CoercionN
-> CoercionN
-> CoercionN
-> CoercionN
FunCo Role
r FunTyFlag
af FunTyFlag
af (Role -> Type -> CoercionN
mkReflCo Role
r Type
w) (Role -> Type -> CoercionN
mkReflCo Role
r Type
ty1) (Role -> Type -> CoercionN
mkReflCo Role
r Type
ty2))
    Just (TyConApp TyCon
tc [Type]
tys, Role
r)
      -> CoercionN -> Maybe CoercionN
forall a. a -> Maybe a
Just (Role -> TyCon -> [CoercionN] -> CoercionN
TyConAppCo Role
r TyCon
tc ((Role -> Type -> CoercionN) -> [Role] -> [Type] -> [CoercionN]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Type -> CoercionN
mkReflCo (Role -> TyCon -> [Role]
tyConRoleListX Role
r TyCon
tc) [Type]
tys))
    Just (ForAllTy (Bndr OutTyVar
tv ForAllTyFlag
_) Type
ty, Role
r)
      -> CoercionN -> Maybe CoercionN
forall a. a -> Maybe a
Just (OutTyVar -> CoercionN -> CoercionN -> CoercionN
ForAllCo OutTyVar
tv (Type -> CoercionN
mkNomReflCo (OutTyVar -> Type
varType OutTyVar
tv)) (Role -> Type -> CoercionN
mkReflCo Role
r Type
ty))
    -- NB: NoRefl variant. Otherwise, we get a loop!
    Maybe (Type, Role)
_ -> Maybe CoercionN
forall a. Maybe a
Nothing

{-
************************************************************************
*                                                                      *
              Flattening
*                                                                      *
************************************************************************

Note [Flattening type-family applications when matching instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As described in "Closed type families with overlapping equations"
http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
we need to flatten core types before unifying them, when checking for "surely-apart"
against earlier equations of a closed type family.
Flattening means replacing all top-level uses of type functions with
fresh variables, *taking care to preserve sharing*. That is, the type
(Either (F a b) (F a b)) should flatten to (Either c c), never (Either
c d).

Here is a nice example of why it's all necessary:

  type family F a b where
    F Int Bool = Char
    F a   b    = Double
  type family G a         -- open, no instances

How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't match,
while the second equation does. But, before reducing, we must make sure that the
target can never become (F Int Bool). Well, no matter what G Float becomes, it
certainly won't become *both* Int and Bool, so indeed we're safe reducing
(F (G Float) (G Float)) to Double.

This is necessary not only to get more reductions (which we might be
willing to give up on), but for substitutivity. If we have (F x x), we
can see that (F x x) can reduce to Double. So, it had better be the
case that (F blah blah) can reduce to Double, no matter what (blah)
is!  Flattening as done below ensures this.

We also use this flattening operation to check for class instances.
If we have
  instance C (Maybe b)
  instance {-# OVERLAPPING #-} C (Maybe Bool)
  [W] C (Maybe (F a))
we want to know that the second instance might match later. So we
flatten the (F a) in the target before trying to unify with instances.
(This is done in GHC.Core.InstEnv.lookupInstEnv'.)

The algorithm works by building up a TypeMap TyVar, mapping
type family applications to fresh variables. This mapping must
be threaded through all the function calls, as any entry in
the mapping must be propagated to all future nodes in the tree.

The algorithm also must track the set of in-scope variables, in
order to make fresh variables as it flattens. (We are far from a
source of fresh Uniques.) See Wrinkle 2, below.

There are wrinkles, of course:

1. The flattening algorithm must account for the possibility
   of inner `forall`s. (A `forall` seen here can happen only
   because of impredicativity. However, the flattening operation
   is an algorithm in Core, which is impredicative.)
   Suppose we have (forall b. F b) -> (forall b. F b). Of course,
   those two bs are entirely unrelated, and so we should certainly
   not flatten the two calls F b to the same variable. Instead, they
   must be treated separately. We thus carry a substitution that
   freshens variables; we must apply this substitution (in
   `coreFlattenTyFamApp`) before looking up an application in the environment.
   Note that the range of the substitution contains only TyVars, never anything
   else.

   For the sake of efficiency, we only apply this substitution when absolutely
   necessary. Namely:

   * We do not perform the substitution at all if it is empty.
   * We only need to worry about the arguments of a type family that are within
     the arity of said type family, so we can get away with not applying the
     substitution to any oversaturated type family arguments.
   * Importantly, we do /not/ achieve this substitution by recursively
     flattening the arguments, as this would be wrong. Consider `F (G a)`,
     where F and G are type families. We might decide that `F (G a)` flattens
     to `beta`. Later, the substitution is non-empty (but does not map `a`) and
     so we flatten `G a` to `gamma` and try to flatten `F gamma`. Of course,
     `F gamma` is unknown, and so we flatten it to `delta`, but it really
     should have been `beta`! Argh!

     Moral of the story: instead of flattening the arguments, just substitute
     them directly.

2. There are two different reasons we might add a variable
   to the in-scope set as we work:

     A. We have just invented a new flattening variable.
     B. We have entered a `forall`.

   Annoying here is that in-scope variable source (A) must be
   threaded through the calls. For example, consider (F b -> forall c. F c).
   Suppose that, when flattening F b, we invent a fresh variable c.
   Now, when we encounter (forall c. F c), we need to know c is already in
   scope so that we locally rename c to c'. However, if we don't thread through
   the in-scope set from one argument of (->) to the other, we won't know this
   and might get very confused.

   In contrast, source (B) increases only as we go deeper, as in-scope sets
   normally do. However, even here we must be careful. The TypeMap TyVar that
   contains mappings from type family applications to freshened variables will
   be threaded through both sides of (forall b. F b) -> (forall b. F b). We
   thus must make sure that the two `b`s don't get renamed to the same b1. (If
   they did, then looking up `F b1` would yield the same flatten var for
   each.) So, even though `forall`-bound variables should really be in the
   in-scope set only when they are in scope, we retain these variables even
   outside of their scope. This ensures that, if we encounter a fresh
   `forall`-bound b, we will rename it to b2, not b1. Note that keeping a
   larger in-scope set than strictly necessary is always OK, as in-scope sets
   are only ever used to avoid collisions.

   Sadly, the freshening substitution described in (1) really mustn't bind
   variables outside of their scope: note that its domain is the *unrenamed*
   variables. This means that the substitution gets "pushed down" (like a
   reader monad) while the in-scope set gets threaded (like a state monad).
   Because a Subst contains its own in-scope set, we don't carry a Subst;
   instead, we just carry a TvSubstEnv down, tying it to the InScopeSet
   traveling separately as necessary.

3. Consider `F ty_1 ... ty_n`, where F is a type family with arity k:

     type family F ty_1 ... ty_k :: res_k

   It's tempting to just flatten `F ty_1 ... ty_n` to `alpha`, where alpha is a
   flattening skolem. But we must instead flatten it to
   `alpha ty_(k+1) ... ty_n`—that is, by only flattening up to the arity of the
   type family.

   Why is this better? Consider the following concrete example from #16995:

     type family Param :: Type -> Type

     type family LookupParam (a :: Type) :: Type where
       LookupParam (f Char) = Bool
       LookupParam x        = Int

     foo :: LookupParam (Param ())
     foo = 42

   In order for `foo` to typecheck, `LookupParam (Param ())` must reduce to
   `Int`. But if we flatten `Param ()` to `alpha`, then GHC can't be sure if
   `alpha` is apart from `f Char`, so it won't fall through to the second
   equation. But since the `Param` type family has arity 0, we can instead
   flatten `Param ()` to `alpha ()`, about which GHC knows with confidence is
   apart from `f Char`, permitting the second equation to be reached.

   Not only does this allow more programs to be accepted, it's also important
   for correctness. Not doing this was the root cause of the Core Lint error
   in #16995.

flattenTys is defined here because of module dependencies.
-}

data FlattenEnv
  = FlattenEnv { FlattenEnv -> TypeMap (OutTyVar, TyCon, [Type])
fe_type_map :: TypeMap (TyVar, TyCon, [Type])
                 -- domain: exactly-saturated type family applications
                 -- range: (fresh variable, type family tycon, args)
               , FlattenEnv -> InScopeSet
fe_in_scope :: InScopeSet }
                 -- See Note [Flattening type-family applications when matching instances]

emptyFlattenEnv :: InScopeSet -> FlattenEnv
emptyFlattenEnv :: InScopeSet -> FlattenEnv
emptyFlattenEnv InScopeSet
in_scope
  = FlattenEnv { fe_type_map :: TypeMap (OutTyVar, TyCon, [Type])
fe_type_map = TypeMap (OutTyVar, TyCon, [Type])
forall a. TypeMap a
emptyTypeMap
               , fe_in_scope :: InScopeSet
fe_in_scope = InScopeSet
in_scope }

updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
updateInScopeSet FlattenEnv
env InScopeSet -> InScopeSet
upd = FlattenEnv
env { fe_in_scope = upd (fe_in_scope env) }

flattenTys :: InScopeSet -> [Type] -> [Type]
-- See Note [Flattening type-family applications when matching instances]
flattenTys :: InScopeSet -> [Type] -> [Type]
flattenTys InScopeSet
in_scope [Type]
tys = ([Type], TyVarEnv (TyCon, [Type])) -> [Type]
forall a b. (a, b) -> a
fst (InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
flattenTysX InScopeSet
in_scope [Type]
tys)

flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
-- See Note [Flattening type-family applications when matching instances]
-- NB: the returned types mention the fresh type variables
--     in the domain of the returned env, whose range includes
--     the original type family applications. Building a substitution
--     from this information and applying it would yield the original
--     types -- almost. The problem is that the original type might
--     have something like (forall b. F a b); the returned environment
--     can't really sensibly refer to that b. So it may include a locally-
--     bound tyvar in its range. Currently, the only usage of this env't
--     checks whether there are any meta-variables in it
--     (in GHC.Tc.Solver.Monad.mightEqualLater), so this is all OK.
flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
flattenTysX InScopeSet
in_scope [Type]
tys
  = let (FlattenEnv
env, [Type]
result) = TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
coreFlattenTys TvSubstEnv
emptyTvSubstEnv (InScopeSet -> FlattenEnv
emptyFlattenEnv InScopeSet
in_scope) [Type]
tys in
    ([Type]
result, TypeMap (OutTyVar, TyCon, [Type]) -> TyVarEnv (TyCon, [Type])
build_env (FlattenEnv -> TypeMap (OutTyVar, TyCon, [Type])
fe_type_map FlattenEnv
env))
  where
    build_env :: TypeMap (TyVar, TyCon, [Type]) -> TyVarEnv (TyCon, [Type])
    build_env :: TypeMap (OutTyVar, TyCon, [Type]) -> TyVarEnv (TyCon, [Type])
build_env TypeMap (OutTyVar, TyCon, [Type])
env_in
      = ((OutTyVar, TyCon, [Type])
 -> TyVarEnv (TyCon, [Type]) -> TyVarEnv (TyCon, [Type]))
-> TypeMap (OutTyVar, TyCon, [Type])
-> TyVarEnv (TyCon, [Type])
-> TyVarEnv (TyCon, [Type])
forall a b. (a -> b -> b) -> TypeMap a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM (\(OutTyVar
tv, TyCon
tc, [Type]
tys) TyVarEnv (TyCon, [Type])
env_out -> TyVarEnv (TyCon, [Type])
-> OutTyVar -> (TyCon, [Type]) -> TyVarEnv (TyCon, [Type])
forall a. VarEnv a -> OutTyVar -> a -> VarEnv a
extendVarEnv TyVarEnv (TyCon, [Type])
env_out OutTyVar
tv (TyCon
tc, [Type]
tys))
               TypeMap (OutTyVar, TyCon, [Type])
env_in TyVarEnv (TyCon, [Type])
forall a. VarEnv a
emptyVarEnv

coreFlattenTys :: TvSubstEnv -> FlattenEnv
               -> [Type] -> (FlattenEnv, [Type])
coreFlattenTys :: TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
coreFlattenTys TvSubstEnv
subst = (FlattenEnv -> Type -> (FlattenEnv, Type))
-> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL (TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
coreFlattenTy TvSubstEnv
subst)

coreFlattenTy :: TvSubstEnv -> FlattenEnv
              -> Type -> (FlattenEnv, Type)
coreFlattenTy :: TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
coreFlattenTy TvSubstEnv
subst = FlattenEnv -> Type -> (FlattenEnv, Type)
go
  where
    go :: FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env Type
ty'

    go FlattenEnv
env (TyVarTy OutTyVar
tv)
      | Just Type
ty <- TvSubstEnv -> OutTyVar -> Maybe Type
forall a. VarEnv a -> OutTyVar -> Maybe a
lookupVarEnv TvSubstEnv
subst OutTyVar
tv = (FlattenEnv
env, Type
ty)
      | Bool
otherwise                        = let (FlattenEnv
env', Type
ki) = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env (OutTyVar -> Type
tyVarKind OutTyVar
tv) in
                                           (FlattenEnv
env', OutTyVar -> Type
mkTyVarTy (OutTyVar -> Type) -> OutTyVar -> Type
forall a b. (a -> b) -> a -> b
$ OutTyVar -> Type -> OutTyVar
setTyVarKind OutTyVar
tv Type
ki)
    go FlattenEnv
env (AppTy Type
ty1 Type
ty2) = let (FlattenEnv
env1, Type
ty1') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env  Type
ty1
                                 (FlattenEnv
env2, Type
ty2') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env1 Type
ty2 in
                             (FlattenEnv
env2, Type -> Type -> Type
AppTy Type
ty1' Type
ty2')
    go FlattenEnv
env (TyConApp TyCon
tc [Type]
tys)
         -- NB: Don't just check if isFamilyTyCon: this catches *data* families,
         -- which are generative and thus can be preserved during flattening
      | Bool -> Bool
not (TyCon -> Role -> Bool
isGenerativeTyCon TyCon
tc Role
Nominal)
      = TvSubstEnv -> FlattenEnv -> TyCon -> [Type] -> (FlattenEnv, Type)
coreFlattenTyFamApp TvSubstEnv
subst FlattenEnv
env TyCon
tc [Type]
tys

      | Bool
otherwise
      = let (FlattenEnv
env', [Type]
tys') = TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
coreFlattenTys TvSubstEnv
subst FlattenEnv
env [Type]
tys in
        (FlattenEnv
env', TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tys')

    go FlattenEnv
env ty :: Type
ty@(FunTy { ft_mult :: Type -> Type
ft_mult = Type
mult, ft_arg :: Type -> Type
ft_arg = Type
ty1, ft_res :: Type -> Type
ft_res = Type
ty2 })
      = let (FlattenEnv
env1, Type
ty1') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env  Type
ty1
            (FlattenEnv
env2, Type
ty2') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env1 Type
ty2
            (FlattenEnv
env3, Type
mult') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env2 Type
mult in
        (FlattenEnv
env3, Type
ty { ft_mult = mult', ft_arg = ty1', ft_res = ty2' })

    go FlattenEnv
env (ForAllTy (Bndr OutTyVar
tv ForAllTyFlag
vis) Type
ty)
      = let (FlattenEnv
env1, TvSubstEnv
subst', OutTyVar
tv') = TvSubstEnv
-> FlattenEnv -> OutTyVar -> (FlattenEnv, TvSubstEnv, OutTyVar)
coreFlattenVarBndr TvSubstEnv
subst FlattenEnv
env OutTyVar
tv
            (FlattenEnv
env2, Type
ty') = TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
coreFlattenTy TvSubstEnv
subst' FlattenEnv
env1 Type
ty in
        (FlattenEnv
env2, VarBndr OutTyVar ForAllTyFlag -> Type -> Type
ForAllTy (OutTyVar -> ForAllTyFlag -> VarBndr OutTyVar ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr OutTyVar
tv' ForAllTyFlag
vis) Type
ty')

    go FlattenEnv
env ty :: Type
ty@(LitTy {}) = (FlattenEnv
env, Type
ty)

    go FlattenEnv
env (CastTy Type
ty CoercionN
co)
      = let (FlattenEnv
env1, Type
ty') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env Type
ty
            (FlattenEnv
env2, CoercionN
co') = TvSubstEnv -> FlattenEnv -> CoercionN -> (FlattenEnv, CoercionN)
coreFlattenCo TvSubstEnv
subst FlattenEnv
env1 CoercionN
co in
        (FlattenEnv
env2, Type -> CoercionN -> Type
CastTy Type
ty' CoercionN
co')

    go FlattenEnv
env (CoercionTy CoercionN
co)
      = let (FlattenEnv
env', CoercionN
co') = TvSubstEnv -> FlattenEnv -> CoercionN -> (FlattenEnv, CoercionN)
coreFlattenCo TvSubstEnv
subst FlattenEnv
env CoercionN
co in
        (FlattenEnv
env', CoercionN -> Type
CoercionTy CoercionN
co')


-- when flattening, we don't care about the contents of coercions.
-- so, just return a fresh variable of the right (flattened) type
coreFlattenCo :: TvSubstEnv -> FlattenEnv
              -> Coercion -> (FlattenEnv, Coercion)
coreFlattenCo :: TvSubstEnv -> FlattenEnv -> CoercionN -> (FlattenEnv, CoercionN)
coreFlattenCo TvSubstEnv
subst FlattenEnv
env CoercionN
co
  = (FlattenEnv
env2, OutTyVar -> CoercionN
mkCoVarCo OutTyVar
covar)
  where
    (FlattenEnv
env1, Type
kind') = TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
coreFlattenTy TvSubstEnv
subst FlattenEnv
env (CoercionN -> Type
coercionType CoercionN
co)
    covar :: OutTyVar
covar         = InScopeSet -> Type -> OutTyVar
mkFlattenFreshCoVar (FlattenEnv -> InScopeSet
fe_in_scope FlattenEnv
env1) Type
kind'
    -- Add the covar to the FlattenEnv's in-scope set.
    -- See Note [Flattening type-family applications when matching instances], wrinkle 2A.
    env2 :: FlattenEnv
env2          = FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
updateInScopeSet FlattenEnv
env1 ((InScopeSet -> OutTyVar -> InScopeSet)
-> OutTyVar -> InScopeSet -> InScopeSet
forall a b c. (a -> b -> c) -> b -> a -> c
flip InScopeSet -> OutTyVar -> InScopeSet
extendInScopeSet OutTyVar
covar)

coreFlattenVarBndr :: TvSubstEnv -> FlattenEnv
                   -> TyCoVar -> (FlattenEnv, TvSubstEnv, TyVar)
coreFlattenVarBndr :: TvSubstEnv
-> FlattenEnv -> OutTyVar -> (FlattenEnv, TvSubstEnv, OutTyVar)
coreFlattenVarBndr TvSubstEnv
subst FlattenEnv
env OutTyVar
tv
  = (FlattenEnv
env2, TvSubstEnv
subst', OutTyVar
tv')
  where
    -- See Note [Flattening type-family applications when matching instances], wrinkle 2B.
    kind :: Type
kind          = OutTyVar -> Type
varType OutTyVar
tv
    (FlattenEnv
env1, Type
kind') = TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
coreFlattenTy TvSubstEnv
subst FlattenEnv
env Type
kind
    tv' :: OutTyVar
tv'           = InScopeSet -> OutTyVar -> OutTyVar
uniqAway (FlattenEnv -> InScopeSet
fe_in_scope FlattenEnv
env1) (OutTyVar -> Type -> OutTyVar
setVarType OutTyVar
tv Type
kind')
    subst' :: TvSubstEnv
subst'        = TvSubstEnv -> OutTyVar -> Type -> TvSubstEnv
forall a. VarEnv a -> OutTyVar -> a -> VarEnv a
extendVarEnv TvSubstEnv
subst OutTyVar
tv (OutTyVar -> Type
mkTyVarTy OutTyVar
tv')
    env2 :: FlattenEnv
env2          = FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
updateInScopeSet FlattenEnv
env1 ((InScopeSet -> OutTyVar -> InScopeSet)
-> OutTyVar -> InScopeSet -> InScopeSet
forall a b c. (a -> b -> c) -> b -> a -> c
flip InScopeSet -> OutTyVar -> InScopeSet
extendInScopeSet OutTyVar
tv')

coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv
                    -> TyCon         -- type family tycon
                    -> [Type]        -- args, already flattened
                    -> (FlattenEnv, Type)
coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv -> TyCon -> [Type] -> (FlattenEnv, Type)
coreFlattenTyFamApp TvSubstEnv
tv_subst FlattenEnv
env TyCon
fam_tc [Type]
fam_args
  = case TypeMap (OutTyVar, TyCon, [Type])
-> Type -> Maybe (OutTyVar, TyCon, [Type])
forall a. TypeMap a -> Type -> Maybe a
lookupTypeMap TypeMap (OutTyVar, TyCon, [Type])
type_map Type
fam_ty of
      Just (OutTyVar
tv, TyCon
_, [Type]
_) -> (FlattenEnv
env', Type -> [Type] -> Type
mkAppTys (OutTyVar -> Type
mkTyVarTy OutTyVar
tv) [Type]
leftover_args')
      Maybe (OutTyVar, TyCon, [Type])
Nothing ->
        let tyvar_name :: Name
tyvar_name = TyCon -> Name
forall a. Uniquable a => a -> Name
mkFlattenFreshTyName TyCon
fam_tc
            tv :: OutTyVar
tv         = InScopeSet -> OutTyVar -> OutTyVar
uniqAway InScopeSet
in_scope (OutTyVar -> OutTyVar) -> OutTyVar -> OutTyVar
forall a b. (a -> b) -> a -> b
$
                         Name -> Type -> OutTyVar
mkTyVar Name
tyvar_name ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
fam_ty)

            ty' :: Type
ty'   = Type -> [Type] -> Type
mkAppTys (OutTyVar -> Type
mkTyVarTy OutTyVar
tv) [Type]
leftover_args'
            env'' :: FlattenEnv
env'' = FlattenEnv
env' { fe_type_map = extendTypeMap type_map fam_ty
                                                       (tv, fam_tc, sat_fam_args)
                         , fe_in_scope = extendInScopeSet in_scope tv }
        in (FlattenEnv
env'', Type
ty')
  where
    arity :: Arity
arity = TyCon -> Arity
tyConArity TyCon
fam_tc
    tcv_subst :: Subst
tcv_subst = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (FlattenEnv -> InScopeSet
fe_in_scope FlattenEnv
env) IdSubstEnv
emptyIdSubstEnv TvSubstEnv
tv_subst CvSubstEnv
forall a. VarEnv a
emptyVarEnv
    ([Type]
sat_fam_args, [Type]
leftover_args) = Bool -> ([Type], [Type]) -> ([Type], [Type])
forall a. HasCallStack => Bool -> a -> a
assert (Arity
arity Arity -> Arity -> Bool
forall a. Ord a => a -> a -> Bool
<= [Type] -> Arity
forall a. [a] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [Type]
fam_args) (([Type], [Type]) -> ([Type], [Type]))
-> ([Type], [Type]) -> ([Type], [Type])
forall a b. (a -> b) -> a -> b
$
                                    Arity -> [Type] -> ([Type], [Type])
forall a. Arity -> [a] -> ([a], [a])
splitAt Arity
arity [Type]
fam_args
    -- Apply the substitution before looking up an application in the
    -- environment. See Note [Flattening type-family applications when matching instances],
    -- wrinkle 1.
    -- NB: substTys short-cuts the common case when the substitution is empty.
    sat_fam_args' :: [Type]
sat_fam_args' = (() :: Constraint) => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys Subst
tcv_subst [Type]
sat_fam_args
    (FlattenEnv
env', [Type]
leftover_args') = TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
coreFlattenTys TvSubstEnv
tv_subst FlattenEnv
env [Type]
leftover_args
    -- `fam_tc` may be over-applied to `fam_args` (see
    -- Note [Flattening type-family applications when matching instances]
    -- wrinkle 3), so we split it into the arguments needed to saturate it
    -- (sat_fam_args') and the rest (leftover_args')
    fam_ty :: Type
fam_ty = TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
sat_fam_args'
    FlattenEnv { fe_type_map :: FlattenEnv -> TypeMap (OutTyVar, TyCon, [Type])
fe_type_map = TypeMap (OutTyVar, TyCon, [Type])
type_map
               , fe_in_scope :: FlattenEnv -> InScopeSet
fe_in_scope = InScopeSet
in_scope } = FlattenEnv
env'

mkFlattenFreshTyName :: Uniquable a => a -> Name
mkFlattenFreshTyName :: forall a. Uniquable a => a -> Name
mkFlattenFreshTyName a
unq
  = Unique -> FastString -> Name
mkSysTvName (a -> Unique
forall a. Uniquable a => a -> Unique
getUnique a
unq) (String -> FastString
fsLit String
"flt")

mkFlattenFreshCoVar :: InScopeSet -> Kind -> CoVar
mkFlattenFreshCoVar :: InScopeSet -> Type -> OutTyVar
mkFlattenFreshCoVar InScopeSet
in_scope Type
kind
  = let uniq :: Unique
uniq = InScopeSet -> Unique
unsafeGetFreshLocalUnique InScopeSet
in_scope
        name :: Name
name = Unique -> FastString -> Name
mkSystemVarName Unique
uniq (String -> FastString
fsLit String
"flc")
    in Name -> Type -> OutTyVar
mkCoVar Name
name Type
kind