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

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

+import GHC.Types.Var( tyVarKind )

+  -- NB: work_args exactly saturate fam_tc

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

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

+                Just (FDEqns { fd_qtvs = qtvs

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

+              -- Do not apply the substitution to `work_tys`;

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

+

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

+      = Just $

+        if all (`elemSubst` subst) branch_qtvs -- See (OTF1)

+        then mkInjectivityFDEqn []          inj_flags

+                                            (substTys subst branch_lhs_tys)

+                                            work_args

+        else mkInjectivityFDEqn branch_qtvs (True:       inj_flags)

+                                            (branch_rhs: branch_lhs_tys)

+                                            (work_rhs:   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

+

+

+{- See Historical Note [trim_qtvs]

+-}

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

+Then, since F has been checked as injective, and the RHS `a->a` (pre-)matches

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

+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 ] }

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

+

+Previously we tried fancy footwork -- see Historical Note [trim_qtvs].

+But now we do the following, given

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

+   type instance F lhs1 lhs2 = rhs

+   [W] F wlhs1 wlhs2 ~ wrhs

+

+* We can safely abandon the sustitution entirely and generate

+      FDEqns{ fd_qtvs = [a,b], fd_eqs = [ lhs2 ~ wlhs2, rhs ~ wrhs ] }

+  By generating (rhs ~ wrhs) we effectively make the solver re-generate the

+  substitution.  This is also what we do for closed type families; see (CF7).

+  These 'fd_qtvs' are subsequently instantiated to fresh meta-variables by

+  'instantiateFunDepEqns'.  See Historical Note [trim_qtvs].

+

+* As a fast-path optimisation, if the substitution (a /matching/ substition only,

+  remember) covers all the `qtvs` of the type instance, there's no hidden-kind problem.

+  Just apply the substitution and equate, with fd_qtvs = []:

+      FDEqns{ fd_qtvs = [], fd_eqs = [ S(lhs2) ~ wlhs2 }

+

+Historical Note [trim_qtvs]

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

+In Note [Exploiting open type families], we previously tried to make use of

+the matching substitution `S`, by defining

+     unbound_qs = qs \ dom(S)

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

+But it turned out to be tricky.  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`.

+

+This fancy footwork for `fd_qtvs` used to be done by `trim_qtvs`.  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

+

+(TQ3) This was hard enough for open type type families, which use matching.

+But it was ridiculously hard for /closed/ type families which use pre-/unification/

+so that the substitution `S` has both meta-tyvars and instance-head tyvars in

+the range.

+

+It's much easier to drop all this and just make fresh meta-tyvars for

+all the quantified type variables.

+  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.  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 ]

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

+  FAR too much: #27994 is an excellent example.  I gave up and now just ignore

+  the substitution, making a fresh meta-var for each quantified variable.

+

+(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, when generating the fundep equations for the solver to deal

+  with, we do /not/ apply the pre-unifying substitution S. 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, [''])