+       -- For a data family (only) cab_tvs and cab_lhs may be eta-reduced

+       -- See Note [Eta reduction for data families]

+

+       -- For a data family `cab_lhs` may be shorter than the arity

+       --     of the data type

+       -- For a type family `cab_lhs` is exactly the family arity

+       -- See Note [Eta reduction for data families]

+

+  canEqLHSKind, canEqLHSType, eqCanEqLHS, saturatedFamApp_maybe

+import GHC.Exts( inline )

+

+scopedSort xs

+  | null xs   = []

+  | otherwise = go [] [] xs

+saturatedFamApp_maybe :: Type -> Maybe (TyCon,[Type])

+saturatedFamApp_maybe xi

+  = Just (tc,args)

+  | otherwise

+  = Nothing

+canTyFamEqLHS_maybe :: Type -> Maybe CanEqLHS

+canTyFamEqLHS_maybe xi

+  | Just (tc, args) <- inline saturatedFamApp_maybe xi

+  = Just $ TyFamLHS tc args

+import GHC.Core.Predicate( saturatedFamApp_maybe )

+isTFHeaded :: Type -> Bool

+isTFHeaded ty = isJust (saturatedFamApp_maybe ty)

+import GHC.Core.TyCo.Subst( deepSubstTy, elemSubst, extendTvSubstWithClone )

+import GHC.Core.Predicate( EqRel(..), saturatedFamApp_maybe )

+import GHC.Types.Var( TyVar, updateVarType, tyVarKind )

+  -- NB: work_args exactly saturate fam_tc

+-- Caller will only use these FunDepEqns if there is just one relevant

+-- equation, i.e. the returned [FunDepEqns] is a singleton.

+                            -- See (RW1)-(RW3) in Note [Relevance]

+            , let lhs_tys' = map (deepSubstTy subst) lhs_tys

+                  -- deepSubstTy: see (CF8) in Note [Exploiting closed type families]

+            = -- Ignore the substitution, except for `noEarlierMatchCheck`

+              Just $

+              if all (`elemSubst` subst) qtvs

+              then -- `subst` eliminates all qtvs; and no qtvs in range of subst

+                   -- See (CF7)(A) in Note [Exploiting closed type families]

+                   FDEqns { fd_qtvs = []

+                          , fd_eqs  = zipWith Pair (substTy subst rhs_ty : lhs_tys')

+                                                   work_tys }

+                          -- Do not apply `subst` to `work_tys`;

+                          -- See (CF9) in Note [Exploiting closed type families]

+

+              else -- Abandon `subst`; re-create it from (rhs_ty ~ work_rhs)

+                   -- See (CF7)(B) in Note [Exploiting closed type families]

+                   FDEqns { fd_qtvs = qtvs

+                          , fd_eqs  = zipWith Pair (rhs_ty:lhs_tys) work_tys }

+

+-- NB: work_args exactly saturate fam_tc

+        -- No need for an apartness check here;

+        -- for open type families there are no "preceding" equations

+        -- Both branch_lhs_tys and work_args exactly saturate fam_tc

+      , let (subst', qtvs') = trimQtvs subst branch_qtvs

+        -- We must apply the substitution here see (OF1)

+      = Just (mkInjectivityFDEqn qtvs' inj_flags branch_lhs_tys' work_args)

+             eqns_from_self = case saturatedFamApp_maybe work_rhs of

+                                Just (tc, rhs_tys) | fam_tc == tc -> [mk_eqn rhs_tys]

+                                _                                 -> []

+    mk_eqn iargs = mkInjectivityFDEqn [] inj_flags work_args iargs

+

+trimQtvs :: Subst -> [TyVar] -> (Subst, [TyVar])

+trimQtvs unif_subst qtvs

+        tv'    = updateVarType (substTy subst) tv

+mkInjectivityFDEqn :: [TcTyVar]             -- Quantify these

+                   -> [Bool]                -- Injectivity flags

+-- The injectivity flags [Bool] will not all be False,

+--   but nothing goes wrong if they are

+mkInjectivityFDEqn qtvs inj_args lhs_args rhs_args

+  = assertPpr (let len = length inj_args in

+               len == length lhs_args && len == length rhs_args)

+              (vcat [ text "inj_args:" <+> ppr inj_args

+                    , text "lhs_args:" <+> ppr lhs_args

+                    , text "rhs_args:" <+> ppr rhs_args ]) $

+    -- Need inj_args lhs_args and rhs_args to be same length for zip3

+    FDEqns { fd_qtvs = qtvs, fd_eqs = eqs }

+For an open type family, generating fundeps from a top-level type instance

+is covered in Section 5.2 in the Injective Type Families paper.

+

+Basic plan: Suppose type family F a b = r | r -> b

+            and Wanted [W] F wlhs1 wlhs2 ~ wrhs

+  Then for each type instance (F lhs1 lhs2 = rhs)

+  * Pre-match `rhs` against `wrhs` to get a substitution S

+  * Generate fundep equalities  S(lhs2) ~ wrhs

+    one for each fundep in the type family 

+

+For example, suppose we have

+   type family F a b = r | r -> a

+   type instance F [a] Int = a->a

+   [W] F alpha beta ~ Int->Int

+Then we pre-match template (a->a) against target (Int->Int) to get

+substitution S = [a :-> Int].  Then we can generate

+Note that `fd_qtvs = []`; we have substituted away the quantifed type variable `a`.

+   type instance F (b -> Maybe a) = [(G a,b)]   -- G is a type family

+   [W] F alpha ~ [(ty,Int)]

+Then, the RHS [(G a,b)] pre-matches with the RHS of the Wanted, but with

+the substitution [b :-> Int], which does not fix `a`.  So, after trimming

+the quantified type variables, we get this FunDepEqns:

+   FDEqns{ fd_qtvs = [a], fd_eqs = [ (Int -> Maybe a) ~ alpha ] }

+   [W] (Int -> Maybe gamma) ~ alpha    -- Fresh gamma

+We have learned that `alpha` must be a list of functions, but that is all;

+we don't know `gamma`.

+

+It gets tricker.  Suppose we have

+   type family F @k a = r | r -> k,a

+   type instance F @k (Proxy @k (a::k)) = T k

+   [W] F alpha beta ~ T Type

+Matching the RHS gives substitution [k :-> Type].   But we do /not/ want

+to end up with this:

+   FDEqns{ fd_qtvs = [a::k], fd_eqs = [ Proxy @Type (a::k) ~ alpha ] }

+because that `k`, hidden inside the kind of `a`, escapes into the solver.

+

+Instead we must not only "trim" the quantified variables of the equation,

+but /substitute/ in the kinds of the leftover quantified ones: see Note [trimQtvs].

+Then we get

+   FDEqns{ fd_qtvs = [a::Type], fd_eqs = [ Proxy @Type (a::Type) ~ alpha ] }

+

+Side note:

+

+You might wonder whether we can use the same solution as we do for /closed/

+families, by generating an equality for the RHSs; see (CF7).  But we can't.

+Example:

+   type family G a where G Int = Char

+   type family F a b = r | r -> a

+   type instance F a   [c]  = (a, G a)      -- (I1)

+   type instance F Int Bool = (Int, Bool)   -- (I2)

+   [W] F alpha Bool ~ (Int,gamma)

+Note that (I1) and (I2) are pariwise-injective: if the RHSs are the same,

+the LHSs are the same /in the injective position(s)/.  See Section 4.2 in

+the "Injective Type Families" paper.  We pre-match (I1) against the Wanted

+giving substitution  [a :-> Int].  We /cannot/ then generate

+   FDEqns { fd_qtvs = [a,c], fd_eqs = [ a~alpha

+                                      , (a,G a)~(Int,gamma) ] }

+where the second equality (wrongly)equates the RHSs.  This is wrong because we

+can solve those fundeps unifying alpha:=Int, gamma:=Char, by reducing (G a) to

+Char.  So we end up with [W] F Int Char, which is insoluble.  Bad.

+

+End of side note.

+

+Note [trimQtvs]

+~~~~~~~~~~~~~~~

+In Note [Exploiting open type families], we needed to "trim" the quantified

+type variables of the axiom, removing ones that are eliminated by the

+auubstitution `S`.  So can we just do this?

+     unbound_qs = qs \ dom(S)

+so that we could make fresh meta-variables for only the unbound `qs`.

+No, we can't. Suppose (TQ1)

+    qs = [ k::*, a::k ]

+    S  = [ k :-> UnliftedType ]

+Then we want

+    unbound_qs = [ a::UnliftedType ]    -- Must apply S to q's kind!!

+

+And (TQ2), although I'm not sure if this can actually happen:

+     qs = [ k::*, a::(k::*), b::(a::k) ]

+     S  = [ k :-> UnliftedType ]

+We want

+     unbound_qs = [ a::UnliftedType, b::(a::UnliftedType) ]

+Note that the occurrence of `a` in b's kind should be replaced by the

+newly-kinded `a` not the original `a::k`.

+

+The function `trimQtvs` does the job.  It

+ * Drops a quantified tyvar that /is/ matched

+ * Substitutes in the kind of a quantified tyvar `a` that is /not/ matched

+ * Adds the substitution [a::k :-> a::S(k)] to the substitution

+

+We only use `trimQtvs` for /open/ families. For /closed/ families where we

+/unify/ (rather than match) the equation with the Wanted, it just doesn't work

+(#27994), because the substitution `S` has both meta-tyvars and instance-head

+tyvars in the range.  See (CF7).

+  This bale-out is implemented in `tryFDEqns`.

+(CF7) Relevance.  The function `getRelevantBranches` finds the relevant branch(es)

+   using the (CFFA).   Given an equation

+       type family F a b where { ...; F lhs1 lhs2 = rhs; ... }

+   is the equation relevant for this Wanted?

+       [W] F wlhs1 wlhs2 ~ wrhs

+  We pre-unify [wrhs,wlhs1,wlhs2] against [rhs,lhs1,lhs2], getting back a

+  substitution `S` that makes the two as equal as poss. This substitution can bind

+  both /quantified/ type variables from the instance, and /unification variables/

+  from the solver. Moreover, both kind of type variable can appear in the range

+  of the substitution.

+

+  That's pretty complicated, so we are very cautious about using the returned

+  substitution `S`.  I had a long struggle (#27994) when we were previously trying to

+  apply that returned substitution as an optimisation.  But because type variables

+  can occur in kinds, it was a losing battle -- I ended up with TyVars from the

+  instance head escaping into the solver.   Consider

+      type F :: forall k. k -> *

+      type instance F k a where

+         F (k->*) (b::k->*) = Int

+      [W] F kappa (alpha::kappa) ~ Int

+  We unify the Wanted with the equation to get the substitution

+      [ kappa :-> k->*,  b :-> (alpha::k->*) ]

+  I tried using `trimQtvs` (see Note [trimQtvs]) but my head hurt

+  FAR too much: #27994 is an excellent example.

+

+  So here's the plan:

+  (A) As a fast-path optimisation, if `S` binds all the quantified variables of

+      the type-family equation (which is common), it's all easy: generate

+         FDEqns { fd_qtvs = []

+                , fd_eqs = [ S(lhs1) ~ wlhs1, S(lhs2) ~ wlhs2, S(rhs) ~ wrhs }

+      Note that we do not apply S to `wlhs1/2` or `wrhs`; see (CF9).

+      And note that `fd_qtvs` is empty, because `S` eliminates all the quantified

+      type variables.

+

+  (B) If not, then /discard `S` entirely/ and instead generate

+        FDEqns { fd_qtvs = qtvs

+               , fd_eqs = [ lhs ~ wlhs1, lhs2 ~ wlhs2, rhs ~ wrhs }

+      Now `instantiateFDEqns` will generate fresh unification variables for the

+      `qtvs` and the solver will in effect reconstruct `S`.

+

+(CF8) When computing relevance (Note [Relevance] (R2)) we use `noEarlierMatch`

+  on S(lhs).  But we must use /deep/ substitution on LHS. Consider

+     type family F (a :: k) r where

+       F @Type (Maybe Bool)              r = r      -- B0

+       F @Type ((f :: Type -> Type) Int) r = Bool   -- B1

+       F @k    ((g :: Type -> k) Int)    r = r      -- B2

+

+     [W] F @Type alpha Char ~ Char

+  The `tcUnifyTysForInjectivity` will return substitution

+      [k :-> Type, r :-> Char, alpha :-> (g :: Type->Type) Int], with g unbound

+  If we used `substTy` on the LHS-tys for B2 we'd get

+      lhs_tys' = [Type, (g :: Type -> k) Int, Char]

+  That's ill-kinded because of the free `k`; and (worse) when `noEarlierMatch` matches

+  lhs_tys' against earlier equations, (B1) will fail to match. So (B2) will be

+  judged relevant, even though it isn't.  Bad, bad. Use deep substitution.

+

+(CF9)  Notice that, in (CF7) when generating the fundep equations for the solver to

+  deal with, we do /not/ apply the pre-unifying substitution `S` to the Wanted types.

+  The types wlhs,wrhs contain meta-variables that we must actually unify! Example

+  We don't want to substitute `alpha` away! In fact we just generate these eqns:

+     FDEqns { fd_qtvs = [a,b], fd_eqs [ [a] ~ alpha

+                                      , Maybe b ~ beta

+                                      , (a, G b) ~ (Int, [gamma]) ] }

+  with `fd_qtvs` being the quantified variables of the equation, the LHSs

+  being the types from the equation and the RHSs being the types from the Wanted.

+  Notice that we thereby uphold the `fd_eqs` invariant in `FDEqns` (see its data

+  type decl).

+    -- The kinds of `qtvs` can have free variables;

+    -- in the FDEqns produced by GHC.Tc.Instance.FunDeps.improveFromInstEnv

+{-# LANGUAGE AllowAmbiguousTypes #-}

+{-# LANGUAGE DataKinds #-}

+{-# LANGUAGE FunctionalDependencies #-}

+{-# LANGUAGE GADTs #-}

+{-# LANGUAGE TypeFamilies #-}

+module  T27994a (l2) where

+

+import Data.Kind (Constraint, Type)

+

+l1 :: [String]

+l1 = ["hello", "world!"]

+

+l2 :: [Int]

+l2 = gmap (HCons length HNil) l1

+

+-----

+

+type HList :: [Type] -> Type

+data HList p where

+  HNil :: HList '[]

+  HCons :: x -> HList xs -> HList (x:xs)

+

+type ($$) :: k -> [Type] -> Type

+type family s $$ p where

+  (s :: Type)      $$ '[]   = s

+  (s :: Type -> k) $$ (a:b) = s a $$ b

+

+type Doms :: [Type] -> [Type]

+type family Doms t where

+  Doms '[]            = '[]

+  Doms ((a -> b) : t) = a : Doms t

+

+type Codoms :: [Type] -> [Type]

+type family Codoms t where

+  Codoms '[]            = '[]

+  Codoms ((a -> b) : t) = b : Codoms t

+

+type GMap :: k -> [Type] -> Constraint

+class GMap (s :: k) t | t -> k where

+  gmap :: HList t -> s $$ Doms t -> s $$ Codoms t

+

+instance GMap [] '[a -> b] where

+  gmap :: HList '[a -> b] -> [a] -> [b]

+  gmap (HCons f HNil) = go

+    where

+      go :: [a] -> [b]

+      go []     = []

+      go (x:xs) = f x : go xs

+{-# LANGUAGE DataKinds, TypeFamilies, PolyKinds, GADTs, AllowAmbiguousTypes #-}

+module T27994 where

+

+import Data.Kind (Type)

+import Data.Proxy (Proxy)

+

+type F :: forall{k}. k -> Type -> Type

+type family F s x where

+   F (s :: Type -> k) (Proxy s) = Int

+

+f :: forall k (s :: k) x. F s x -> x

+f _ = undefined

+

+g :: Proxy Maybe -> ()

+g _ = ()

+

+data T a where

+  MkT :: T Int

+

+test :: T a -> ()

+test t = (\y -> case t of MkT -> g y) (f (3 :: Int))

+

+{- [W] F @k_azX (s_azY::k_azX) p_azN ~ Int

+

+unify   [*->k,      s::*->k,  Proxy @(*->k) (s::*->k), Int]

+          ~ [k_azX, s_azY::k_azX, p_azN,                   Int]

+

+  -->   [ k_azX :-> (* -> k)

+        , s     :-> s_azY::k_azX

+        , p_azN :-> Proxy @(*->k) (s::*->k) ]

+

+  fixpt -->   [ k_azX :-> Type -> k

+              , s     :-> s_azY::(Type -> k)

+              , p_azN :-> Proxy @(Type->k) (s::k_azX) ]

+

+Generate a [W] for each pair

+    [W] k ~ k_azX

+    [W] s ~ s_azY

+    [W] Proxy s ~ p_azN

+    [W] Int ~ Int

+As an opt (claim) apply subst first

+    [W] k_azX ~ k_azX

+    [W] s_azY ~ s_azY

+    [W] Proxy s_azY ~ p_azN

+    [W] Int ~ Int

+

+-- [W] F @k_azX s_azY[tau] p_azN ~ Int

+-- Want: fresh k' s'

+-- [W] k' ~ k_azX

+-- [W] s':k' ~ s_azY:k_azX

+-- [W] Proxy s' ~ x

+-}

+

+test('T27994',  normal, compile, [''])

+test('T27994a', normal, compile, [''])