GitLab

Simon Peyton Jones pushed to branch wip/T27994 at Glasgow Haskell Compiler / GHC

Commits:

ed2fd53d

by Simon Peyton Jones at 2026-10-29T00:07:13+00:00

Make niFixSubst idempotent

I discovered (when fixing #27994) that `niFixSubst` didn't actually
generate an idempotent subsitution despite its claims.  It could
return a substitution that mentions domain variables on in its range,
when those variables are hidden inside the kind of a type variable
occurrence.  As a result it can generate ill-kinded types. Boo!

The fix is simple, and uses deep substitution.
See Note [Finding the substitution fixpoint]

I don't think it actually /caused/ any bugs, so there is no
regression test.

ecc5ab3d

by Simon Peyton Jones at 2026-10-29T00:07:13+00:00

Fix a nasty bug in fundeps

This MR fixes #27994, which turned out to be very tricky.

See Note [Exploiting closed type famililes], especially (CF7).  I was
ending up with TyVars (not TcTyVars) in the solver, because the
substitution computed in `getRelevantBranches` mixed the two.

The code was just too clever. I ended up simplifying it quite a bit,
eliminating fancy footwork in a function `trim_qtvs`.  I left behind
Historical Note [trim_qtvs] to explain.

This patch also fixes one other buglet in the same code.

* Over-saturated type families were being mis-handled.
  See the new use of `saturatedFamApp_maybe`.

11 changed files:

compiler/GHC/Core/Coercion/Axiom.hs
compiler/GHC/Core/Predicate.hs
compiler/GHC/Core/TyCo/FVs.hs
compiler/GHC/Core/TyCo/Subst.hs
compiler/GHC/Core/Type.hs
compiler/GHC/Core/Unify.hs
compiler/GHC/Tc/Instance/Family.hs
compiler/GHC/Tc/Solver/FunDeps.hs
+ testsuite/tests/typecheck/should_compile/T27994.hs
+ testsuite/tests/typecheck/should_compile/T27994a.hs
testsuite/tests/typecheck/should_compile/all.T

Changes:

compiler/GHC/Core/Coercion/Axiom.hs

@@ -277,8 +277,8 @@ data CoAxBranch
         -- See Note [CoAxBranch type variables]
      , cab_eta_tvs  :: [TyVar]
         -- ^ Eta-reduced tyvars
 -       -- cab_tvs and cab_lhs may be eta-reduced; see
 -       -- Note [Eta reduction for data families]
 +       -- For a data family (only) cab_tvs and cab_lhs may be eta-reduced
 +       -- See Note [Eta reduction for data families]
      , cab_cvs      :: [CoVar]
        -- ^ Bound coercion variables
         -- Always empty, for now.
@@ -286,8 +286,14 @@ data CoAxBranch
         -- in GHC.Tc.TyCl
      , cab_roles    :: [Role]
         -- ^ See Note [CoAxBranch roles]
++
      , cab_lhs      :: [Type]
         -- ^ Type patterns to match against
 +       -- 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]
++
      , cab_rhs      :: Type
         -- ^ Right-hand side of the equality
         -- See Note [CoAxioms are homogeneous]

compiler/GHC/Core/Predicate.hs

@@ -36,7 +36,7 @@ module GHC.Core.Predicate (
    -- Equality left-hand sides
    CanEqLHS(..), canEqLHS_maybe, canTyFamEqLHS_maybe,
 -  canEqLHSKind, canEqLHSType, eqCanEqLHS
 +  canEqLHSKind, canEqLHSType, eqCanEqLHS, saturatedFamApp_maybe
    ) where
@@ -61,6 +61,8 @@ import GHC.Utils.Misc
  import GHC.Utils.Panic
  import GHC.Data.FastString
 +import GHC.Exts( inline )
++
  {- *********************************************************************
  *                                                                      *
@@ -700,7 +702,9 @@ types/kinds are fully settled and zonked.
  -- See also Note [Ordering of implicit variables] in "GHC.Rename.HsType"
  scopedSort :: [Var] -> [Var]
 -scopedSort = go [] []
 +scopedSort xs
 +  | null xs   = []
 +  | otherwise = go [] [] xs
    where
      go :: [Var] -- already sorted, in reverse order
         -> [TyCoVarSet] -- each set contains all the variables which must be placed
@@ -781,13 +785,19 @@ canEqLHS_maybe xi
    | otherwise
    = canTyFamEqLHS_maybe xi
 -canTyFamEqLHS_maybe :: Type -> Maybe CanEqLHS
 -canTyFamEqLHS_maybe xi
 +saturatedFamApp_maybe :: Type -> Maybe (TyCon,[Type])
 +saturatedFamApp_maybe xi
    | Just (tc, args) <- tcSplitTyConApp_maybe xi
    , isTypeFamilyTyCon tc
    , args `lengthIs` tyConArity tc
 -  = Just $ TyFamLHS tc args
 +  = Just (tc,args)
 +  | otherwise
 +  = Nothing
 +canTyFamEqLHS_maybe :: Type -> Maybe CanEqLHS
 +canTyFamEqLHS_maybe xi
 +  | Just (tc, args) <- inline saturatedFamApp_maybe xi
 +  = Just $ TyFamLHS tc args
    | otherwise
    = Nothing

compiler/GHC/Core/TyCo/FVs.hs

@@ -1159,10 +1159,12 @@ nice tight loops.
  {-# INLINE afvFolder #-}   -- See Note [Any-free-var folder]
  afvFolder :: TyCoFolder (FV (BoundVars, TyCoVar -> Bool) DM.Any)
  -- 'afvFolder' is short for "any-free-var folder", good for checking
 ---   if any /deep/ free var of a type satisfies a predicate `check_fv`
 +--   if any /shallow/ free var of a type satisfies a predicate `check_fv`
  -- The "env" of the (FV env Any) is a pair (bvs,pred) of
  --    the bound variables (which are definitely not free), and
  --    an "interesting var" predicate which the client supplies
 +--
 +-- You can get "deep" by supplying a predicate that also looks in the kind
  afvFolder = TyCoFolder { tcf_view = noView  -- See Note [Free vars and synonyms]
                         , tcf_tyvar = do_tcv
                         , tcf_covar = do_tcv
@@ -1173,8 +1175,7 @@ afvFolder = TyCoFolder { tcf_view = noView  -- See Note [Free vars and synonyms]
      -- Check the variable itself with check_fv,
      -- and check its kind (this is a deep folder)
      do_tcv tcv = MkFV $ \ (bvs,check_fv) ->
 -                 Any (not (tcv `elemVarSet` bvs) &&
 -                      (check_fv tcv || runAny check_fv (afv_type (varType tcv))))
 +                 Any (not (tcv `elemVarSet` bvs) && check_fv tcv)
      do_hole hole = do_tcv (coHoleCoVar hole)
  afv_type  :: Type     -> FV (BoundVars, TyVar -> Bool) DM.Any
@@ -1186,16 +1187,32 @@ runAny :: (TyVar -> Bool) -> FV (BoundVars, TyCoVar -> Bool) DM.Any -> Bool
  {-# INLINE runAny #-}
  runAny check_fv fvs = DM.getAny (runFV fvs (emptyVarSet, check_fv))
 +---------------------------------------------
 +-- anyShallowFreeVarsOfType and friends look only for shallow free vars
 +--    (Currently not needed, left here in case we need it one day)
 +-- anyShallowFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool
 +-- {-# INLINE anyShallowFreeVarsOfType #-}
 +-- anyShallowFreeVarsOfType check_fv ty = runAny check_fv (afv_type ty)
++
 +---------------------------------------------
 +-- anyFreeVarsOfType and friends look for deep free vars
++
 +deep_check :: (TyCoVar -> Bool) -> TyCoVar -> Bool
 +-- This is inefficient because if one tyvar occurs many times
 +-- in a type, it'll look in its kind at each occurrence. Boo.
 +deep_check check_fv tcv = check_fv tcv || anyFreeVarsOfType check_fv (varType tcv)
++
  anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool
  {-# INLINE anyFreeVarsOfType #-}
 -anyFreeVarsOfType check_fv ty = runAny check_fv (afv_type ty)
 +-- Looks deeply, into the kinds of the free vars
 +anyFreeVarsOfType check_fv ty = runAny (deep_check check_fv) (afv_type ty)
  anyFreeVarsOfTypes :: (TyCoVar -> Bool) -> [Type] -> Bool
  {-# INLINE anyFreeVarsOfTypes #-}
 -anyFreeVarsOfTypes check_fv tys = runAny check_fv (afv_types tys)
 +anyFreeVarsOfTypes check_fv tys = runAny (deep_check check_fv) (afv_types tys)
  anyFreeVarsOfCo :: (TyCoVar -> Bool) -> Coercion -> Bool
 -anyFreeVarsOfCo check_fv co = runAny check_fv (afv_co co)
 +anyFreeVarsOfCo check_fv co = runAny (deep_check check_fv) (afv_co co)
  noFreeVarsOfType :: Type -> Bool
  noFreeVarsOfType ty = not $ runAny (const True) (afv_type ty)
@@ -1206,6 +1223,7 @@ noFreeVarsOfTypes tys = not $ runAny (const True) (afv_types tys)
  noFreeVarsOfCo :: Coercion -> Bool
  noFreeVarsOfCo co = not $ runAny (const True) (afv_co co)
++
  {-
  ************************************************************************
  *                                                                      *

compiler/GHC/Core/TyCo/Subst.hs

@@ -48,6 +48,8 @@ module GHC.Core.TyCo.Subst
          substTyCoBndr,
          substVarBndrUsing,
          checkValidSubst, isValidTCvSubst,
++
 +        deepSubstTy
    ) where
  import GHC.Prelude
@@ -775,9 +777,15 @@ substThetaUnchecked = substTysUnchecked
  -- building no thunks.  See Note [Specialising mappers] in GHC.Core.TyCo.Make
  type SubstM = StrictReaderT Subst StrictIdentity
 -runSubstM :: SubstM a -> Subst -> a
 -runSubstM m subst = runStrictIdentity (runStrictReaderT m subst)
 +runSubstM :: forall a. (a -> SubstM a) -> Subst -> a -> a
  {-# INLINE runSubstM #-}
 +runSubstM tx subst x = runStrictIdentity (runStrictReaderT (tx x) subst)
++
 +subst_ty :: Subst -> Type -> Type
 +subst_co :: Subst -> Coercion -> Coercion
 +(subst_ty, subst_co)
 +  = case mapTyCo substTyCoMapper of
 +      (ms_ty, _, ms_co, _) -> (runSubstM ms_ty, runSubstM ms_co)
  substTyCoMapper :: TyCoMapper SubstM
  substTyCoMapper
@@ -785,8 +793,8 @@ substTyCoMapper
                 , tcm_covar      = subst_cv
                 , tcm_hole       = subst_ch
                 , tcm_tycobinder = tcv_bndr
 -               , tcm_tcapp_ty   = tcapp_ty
 -               , tcm_tcapp_co   = tcapp_co
 +               , tcm_tcapp_ty   = nopTcAppTy
 +               , tcm_tcapp_co   = nopTcAppCo
+                }
   where
     subst_tv tv = StrictReaderT $ \subst -> return (substTyVar  subst tv)
@@ -802,23 +810,15 @@ substTyCoMapper
     -- Avoid allocation in this very
     -- common case (E.g. Int, LiftedRep etc)
 -   tcapp_ty :: Type -> TyCon -> [Type] -> SubstM Type
 -   tcapp_ty ty tc tys'
 -      | null tys'  = return ty
 -      | otherwise  = return (mkTyConApp tc tys')
 -   tcapp_co :: Coercion -> Role -> TyCon -> [Coercion] -> SubstM Coercion
 -   tcapp_co co r tc cos'
 -      | null cos'  = return co
 -      | otherwise  = return (mkTyConAppCo r tc cos')
 +nopTcAppTy :: Type -> TyCon -> [Type] -> SubstM Type
 +nopTcAppTy  ty tc tys'
 +  | null tys'  = return ty
 +  | otherwise  = return (mkTyConApp tc tys')
 -subst_ty :: Subst -> Type -> Type
 -subst_co :: Subst -> Coercion -> Coercion
 -(subst_ty, subst_co)
 -  = case mapTyCo substTyCoMapper of
 -      (ms_ty, _, ms_co, _) -> (run ms_ty, run ms_co)
 -  where
 -    run :: forall a. (a -> SubstM a) -> Subst -> a -> a
 -    run ms subst x = runSubstM (ms x) subst
 +nopTcAppCo :: Coercion -> Role -> TyCon -> [Coercion] -> SubstM Coercion
 +nopTcAppCo co r tc cos'
 +  | null cos'  = return co
 +  | otherwise  = return (mkTyConAppCo r tc cos')
  substTyVar :: Subst -> TyVar -> Type
  substTyVar (Subst _ _ tenv _) tv
@@ -1019,3 +1019,75 @@ it is /very/ valuable to /keep/ it empty:
    If the substitution is empty, this is a no-op -- but only if it
    is empty!
  -}
++
++
 +{- **********************************************************************
 +%*                                                                      *
 +                Deep substitution
 +%*                                                                      *
 +%********************************************************************* -}
++
 +{- Note [Deep substitution]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~
 +Deep substitution applies the substitution to the /kinds/ of un-substituted
 +type variables.  Suppose the substitution is
 +    [ k :-> Type ]
 +and we apply it to the type
 +    Proxy k (a :: k)
 +Ordinary shallow substitution will give
 +    Proxy Type (a :: k)
 +which is ill-kinded.  Deep substitution will give
 +    Proxy Type (a :: Type)
++
 +Ordinary (shallow) substitution is usually fine, because we will substitute for
 +`a` as well, but not always.  In particular, the pure unifier in in GHC.Core.Unify
 +uses `niFixSubst` to find a fixpoint, and we really don't want domain tyvars
 +appearing in the range.See Note [Finding the substitution fixpoint].
++
 +Deep substitution risks being rather inefficient because it re-applies the
 +subsitution to the kind at /each occurrence/ of a free variable.  We could
 +perhaps find the free vars, and build a re-kinding substitution, but that's a
 +bit more complicated.
 +-}
++
 +deepSubstTyCoMapper :: TyCoMapper SubstM
 +deepSubstTyCoMapper
 +  = TyCoMapper { tcm_tyvar      = subst_tv
 +               , tcm_covar      = subst_cv
 +               , tcm_hole       = subst_ch
 +               , tcm_tycobinder = tcv_bndr
 +               , tcm_tcapp_ty   = nopTcAppTy
 +               , tcm_tcapp_co   = nopTcAppCo
 +               }
 + where
 +   subst_tv tv = StrictReaderT $ \subst -> return (deepSubstTyVar  subst tv)
 +   subst_cv cv = StrictReaderT $ \subst -> return (deepSubstCoVar  subst cv)
 +   subst_ch ch = StrictReaderT $ \subst -> return (deepSubstCoHole subst ch)
++
 +   tcv_bndr :: TyCoVar -> ForAllTyFlag -> (TyCoVar -> SubstM r) -> SubstM r
 +   tcv_bndr tcv _vis k
 +     = StrictReaderT $ \subst ->
 +       let !(subst', tcv') = substVarBndrUsing deepSubstTy subst tcv
 +       in runStrictReaderT (k tcv') subst'
++
 +deepSubstTy :: Subst -> Type -> Type
 +deepSubstTy = case mapTyCo deepSubstTyCoMapper of
 +                (subst_ty, _, _, _) -> runSubstM subst_ty
++
 +deepSubstTyVar :: Subst -> TyVar -> Type
 +deepSubstTyVar subst@(Subst _ _ tenv _) tv
 +  = assert (isTyVar tv) $
 +    case lookupVarEnv tenv tv of
 +      Just ty -> ty
 +      Nothing -> TyVarTy (updateVarType (deepSubstTy subst) tv)
++
 +deepSubstCoVar :: Subst -> CoVar -> Coercion
 +deepSubstCoVar subst@(Subst _ _ _ cenv) cv
 +  = case lookupVarEnv cenv cv of
 +      Just co -> co
 +      Nothing -> CoVarCo (updateVarType (deepSubstTy subst) cv)
++
 +deepSubstCoHole :: Subst -> CoercionHole -> Coercion
 +-- See Note [Substituting in a coercion hole]
 +deepSubstCoHole subst h@(CH { ch_co_var = cv })
 +  = HoleCo (h { ch_co_var = updateVarType (deepSubstTy subst) cv })

compiler/GHC/Core/Type.hs

@@ -483,7 +483,7 @@ expandTypeSynonyms ty
  expandTypeSynonymsX :: Subst -> Type -> Type
  expandTypeSynonymsX
    = case mapTyCo expandTypeSynonymMapper of
 -      (exp_ty, _, _, _) -> \subst ty -> runSubstM (exp_ty ty) subst
 +      (exp_ty, _, _, _) -> runSubstM exp_ty
  expandTypeSynonymMapper :: TyCoMapper SubstM
  -- Just like substitution, but treat TyConApp specially

compiler/GHC/Core/Unify.hs

@@ -28,13 +28,12 @@ import GHC.Types.Var.Env
  import GHC.Types.Var.Set
  import GHC.Core.Type     hiding ( getTvSubstEnv )
  import GHC.Core.Coercion hiding ( getCvSubstEnv )
 -import GHC.Core.Predicate( scopedSort )
  import GHC.Core.TyCon
  import GHC.Core.Predicate( CanEqLHS(..), canEqLHS_maybe )
  import GHC.Core.TyCon.Env
  import GHC.Core.TyCo.Rep
  import GHC.Core.TyCo.Compare ( eqType, tcEqType, tcEqTyConAppArgs )
 -import GHC.Core.TyCo.Subst   ( mkTvSubst )
 +import GHC.Core.TyCo.Subst   ( mkTvSubst, deepSubstTy )
  import GHC.Core.Map.Type
  import GHC.Core.Multiplicity
@@ -1063,21 +1062,31 @@ During unification we use a TvSubstEnv/CvSubstEnv pair that is
  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
 +We want an /idempotent/ substitution, so `niFixSubst` takes a non-idempotent
 +one and composes it with itself until it becomes idempotent.  Thus if the original
 +is S0, we compute S1 = S0 o S0, S2 = S1 o S1, etc.
++
 +A variable chain v0 :-> v1 :-> ... :-> vm therefore takes about log2 m rounds,
 +The unifier can build such. For example:
 +    (a, a, a, ..., a)   ~   (x1, x2, x3, ..., xm)
 +produces a :-> x1, x1 :-> x2, ..., x(m-1) :-> xm.
++
 +Finding the fixpoint 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) ]
 +This isn't idempotent: it mentions `k` in the range.
++
  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.
 +because (H * (f:k)) is itself ill-kinded, and `typeKind` will fail.
  This happened, for example, in #9106.
 +So (yuckily) we must also substitute inside f's kind, to get
 +   [ k -> *
 +   , g -> H * (f:*) ]
  It gets worse.  In #14164 we wanted to take the fixpoint of
  this substitution
@@ -1090,84 +1099,45 @@ 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 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.
 +Ugh!  This whole thing is pretty horrible. But the solution is simple enough:
++
 +        Use deep substitution (deepSubstTy)
++
 +(deepSubst `s` (Proxy k (a::k)) applies the substitution `s` not only to
 +the occurrence of `k` in the argument of `Proxy`, but also to the `k` inside
 +the kind of `a`.  See Note [Deep substitution] in GHC.Core.TyCo.Subst.
++
 +So `niFixSubst` just applies the substitution /deeply/ to the types in its
 +range, until we reach a fixed point.  Easy!
  -}
  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 in_scope tenv
 -  | not_fixpoint = niFixSubst in_scope (mapVarEnv (substTy subst) tenv)
 -  | otherwise    = tenv_subst
 +  | isEmptyVarEnv tenv     -- Fast path for common case
 +  = mkEmptySubst in_scope
 +  | otherwise
 +  =  -- pprTrace "niFixSubst" (vcat [ text "In: " <+> ppr tenv
 +     --                             , text "Out:" <+> ppr (S.getTvSubstEnv subst) ])
 +     subst
    where
 -    tenv_subst = mkTvSubst in_scope tenv   -- This is our starting point
+-
 -    range_tvs :: [TyVar]
 -    range_tvs = nonDetVarSetElems $
 -                tyCoVarsOfTypes $
 -                nonDetEltsUFM tenv
 -          -- It's OK to use nonDetEltsUFM (twice) here because
 -          -- the order of range_tvs is immaterial
+-
 -    not_fixpoint  = any in_domain range_tvs
 -    in_domain tv  = tv `elemVarEnv` tenv
+-
 -    free_tvs = scopedSort (filterOut in_domain range_tvs)
 +     subst = niFixSubst' 1 in_scope tenv
 -    -- See Note [Finding the substitution fixpoint], Step 6
 -    subst = foldl' add_free_tv tenv_subst free_tvs
+-
 -    add_free_tv :: Subst -> TyVar -> Subst
 -    add_free_tv subst tv
 -      | isTyVar tv = extendTvSubst subst tv (mkTyVarTy tv')
 -      | otherwise  = subst  -- Ignore free coercion variables
 -     where
 -        tv' = updateTyVarKind (substTy subst) tv
 +niFixSubst' :: Int -> InScopeSet -> TvSubstEnv -> Subst
 +niFixSubst' n in_scope tenv_orig
 +  | fixpoint_found = mkTvSubst in_scope tenv_orig
 +  | otherwise      = niFixSubst' (n+1) in_scope tenv_new
 +  where
 +    in_dom tv = tv `elemVarEnv` tenv_orig
 +    tenv_new  = mapVarEnv (deepSubstTy subst) tenv_orig
 +    subst     = mkTvSubst in_scope tenv_orig
++
 +    fixpoint_found = nonDetStrictFoldUFM and_fix True tenv_orig
 +    and_fix :: Type -> Bool -> Bool
 +    and_fix _ False = False
 +    and_fix ty _    = not (anyFreeVarsOfType in_dom ty)
  {-
  ************************************************************************

compiler/GHC/Tc/Instance/Family.hs

@@ -16,6 +16,7 @@ import GHC.Prelude
  import GHC.Driver.DynFlags
  import GHC.Driver.Env
 +import GHC.Core.Predicate( saturatedFamApp_maybe )
  import GHC.Core.FamInstEnv
  import GHC.Core.Coercion
  import GHC.Core.TyCon
@@ -715,15 +716,9 @@ reportInjectivityErrors dflags fi_ax axiom inj
         when wrong_bare_rhs $ reportBareVariableInRHSErr   fam_tc bare_variables axiom
  -- | Is type headed by a type family application?
 -isTFHeaded :: Type -> Bool
  -- See Note [Verifying injectivity annotation], case 3.
 -isTFHeaded ty | Just ty' <- coreView ty
 -              = isTFHeaded ty'
 -isTFHeaded ty | (TyConApp tc args) <- ty
 -              , isTypeFamilyTyCon tc
 -              = args `lengthIs` tyConArity tc
 -isTFHeaded _  = False
+-
 +isTFHeaded :: Type -> Bool
 +isTFHeaded ty = isJust (saturatedFamApp_maybe ty)
  -- | If a RHS is a bare type variable return a set of LHS patterns that are not
  -- bare type variables.

compiler/GHC/Tc/Solver/FunDeps.hs

@@ -24,16 +24,16 @@ import GHC.Tc.Types.Constraint
  import GHC.Core.FamInstEnv
  import GHC.Core.Coercion
  import GHC.Core.TyCo.Rep( Type(..) )
 -import GHC.Core.Predicate( EqRel(..) )
 +import GHC.Core.TyCo.Subst( deepSubstTy )
 +import GHC.Core.Predicate( EqRel(..), saturatedFamApp_maybe )
  import GHC.Core.TyCon
  import GHC.Core.Unify( AmIUnifying(..)
                       , tcUnifyTysForInjectivity, typeListsAreApart )
  import GHC.Core.Coercion.Axiom
 -import GHC.Core.TyCo.Subst( elemSubst, extendTvSubstWithClone )
  import GHC.Builtin.WiredIn.TypeLits( tryInteractTopFam, tryInteractInertFam )
 -import GHC.Types.Var( TyVar, tyVarKind, setTyVarKind )
 +import GHC.Types.Var( tyVarKind )
  import GHC.Types.Var.Set
  import GHC.Types.Var.Env( mkInScopeSet )
@@ -57,7 +57,6 @@ Here is our plan for dealing with functional dependencies
         * send the current constraint back to the start of the pipeline;
           it might now be soluble, and it probably isn't inert
+-
  * Once a unification is done, it can't be un-done.  So we must be very careful
    not to threaten completeness by doing a unification when there might be
    another way to solve the constraint.
@@ -613,6 +612,7 @@ tryFamEqFunDeps mode eqs_for_me fam_tc work_args
  mkTopFamEqFDs :: TyCon -> [TcType] -> EqCt -> SolverStage [FunDepEqns]
  mkTopFamEqFDs fam_tc work_args work_item
 +  -- NB: work_args exactly saturate fam_tc
    | isOpenTypeFamilyTyCon fam_tc
    , Injective inj_flags <- tyConInjectivityInfo fam_tc
    = -- Open, injective type families
@@ -709,24 +709,24 @@ getRelevantBranches ax work_args work_rhs
                                          , cab_lhs = lhs_tys
                                          , cab_rhs = rhs_ty })
              | Just subst <- tcUnifyTysForInjectivity Unifying (rhs_ty:lhs_tys) work_tys
 -              -- See (RW1)-(RW3) in Note [Relevance]
 -              -- This is a pre-/unification/ check (not matching)
 -              -- so `subst` can bind both `qtvs` and fvs(work_tys)
 -            , let (subst',qtvs') = trim_qtvs subst qtvs
 -                  lhs_tys'       = substTys subst' lhs_tys
 -                  rhs_ty'        = substTy  subst' rhs_ty
 -                  branch_tys'    = rhs_ty' : lhs_tys'
 +                            -- See (RW1)-(RW3) in Note [Relevance]
 +            , let lhs_tys' = map (deepSubstTy subst) lhs_tys
 +                  -- deepSubstTy: see (CF8) in Note [Exploiting closed type families]
              , noEarlierMatchCheck lhs_tys' branch  -- See (RW4) in Note [Relevance]
 -            = Just (FDEqns { fd_qtvs = qtvs'
 -                           , fd_eqs  = zipWith Pair branch_tys' work_tys })
 -                              -- Do not apply the substition to `work_tys`;
 -                              -- See (CF7) 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]
++
              | otherwise
              = Nothing
  mkTopOpenFamEqFDs :: TyCon -> [Bool] -> [TcType] -> EqCt -> TcS [FunDepEqns]
  -- Implements (INJFAM:Wanted/top-open)
  -- See Note [Exploiting open type families]
 +-- NB: work_args exactly saturate fam_tc
  mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs })
    = do { fam_envs <- getFamInstEnvs
         ; let branches :: [CoAxBranch]
@@ -738,12 +738,11 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs })
      do_one (CoAxBranch { cab_tvs = branch_qtvs
                         , cab_lhs = branch_lhs_tys
                         , cab_rhs = branch_rhs })
 -      | Just subst <- tcUnifyTysForInjectivity Matching [branch_rhs] [work_rhs]
 -      , let (subst', qtvs') = trim_qtvs subst branch_qtvs
 -            branch_lhs_tys' = substTys subst' branch_lhs_tys
 -        -- No need for an apartness check here; for open type families
 -        -- there are no "preceding" equations
 -      = Just (mkInjectivityFDEqn inj_flags qtvs' branch_lhs_tys' work_args)
 +      | Just {} <- tcUnifyTysForInjectivity Matching [branch_rhs] [work_rhs]
 +        -- 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 (mkInjectivityFDEqn branch_qtvs inj_flags branch_lhs_tys work_args)
        | otherwise
        = Nothing
@@ -756,9 +755,9 @@ mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs
    = do { let -- eqns_from_inerts: see (INJFAM:Wanted/other)
               eqns_from_inerts = mapMaybe do_one eqs_for_me
               -- eqns_from_self: see (INJFAM:Wanted/Self)
 -             eqns_from_self   = case tcSplitTyConApp_maybe work_rhs of
 -                                  Just (tc,rhs_tys) | tc==fam_tc -> [mk_eqn rhs_tys]
 -                                  _                              -> []
 +             eqns_from_self = case saturatedFamApp_maybe work_rhs of
 +                                Just (tc, rhs_tys) | fam_tc == tc -> [mk_eqn rhs_tys]
 +                                _                                 -> []
         ; return (eqns_from_inerts ++ eqns_from_self) }
    where
@@ -768,7 +767,10 @@ mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs
        | otherwise                     = Nothing
      do_one _ = pprPanic "interactFunEq 2" (ppr fam_tc)  -- TyVarLHS
 -    mk_eqn iargs = mkInjectivityFDEqn inj_flags [] work_args iargs
 +    mk_eqn iargs = mkInjectivityFDEqn [] inj_flags work_args iargs
++
++
 +{- See Historical Note [trim_qtvs]
  trim_qtvs :: Subst -> [TyVar] -> (Subst, [TyVar])
  -- Tricky stuff: see (OF1) in Note [Exploiting open type families]
@@ -790,7 +792,7 @@ trim_qtvs unif_subst qtvs
          subst' = extendTvSubstWithClone subst tv tv'
                   -- extendTvSubstWithClone: see (OF1b) in
                   -- Note [Exploiting open type families]
+-
 +-}
  -----------------------------------------
  --  Built-in type families
@@ -883,15 +885,22 @@ mkLocalBuiltinFamEqFDs eqs_for_me fam_tc ops work_args work_rhs
         ; return (eqns_from_inerts ++ eqns_from_self) }
  --------------------
 -mkInjectivityFDEqn :: [Bool]       -- Injectivity flags
 -                   -> [TcTyVar]    -- Quantify these
 +mkInjectivityFDEqn :: [TcTyVar]             -- Quantify these
 +                   -> [Bool]                -- Injectivity flags
                     -> [TcType] -> [TcType]  -- Make these equal
                     -> FunDepEqns
  -- When F s1 s2 s3 ~ F t1 t2 t3, and F has injectivity info [True,False,True]
  --   return the FDEqns { fd_eqs = [Pair s1 t1, Pair s3 t3] }
 --- The injectivity flags [Bool] will not all be False, but nothing goes wrong if they are
 -mkInjectivityFDEqn inj_args qtvs lhs_args rhs_args
 -  = FDEqns { fd_qtvs = qtvs, fd_eqs = eqs }
 +-- 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 }
    where
      eqs = [ Pair lhs_arg rhs_arg
            | (True, lhs_arg, rhs_arg) <- zip3 inj_args lhs_args rhs_args ]
@@ -1104,7 +1113,7 @@ the Injective Type Families paper. For open type families, suppose we have
     [W] F alpha ~ Int->Int
 -Then, since F has been checked as injective, and the RHS `a->a` (pre-)unifies
 +Then, since F has been checked as injective, and the RHS `a->a` (pre-)matches
  with the `Int->Int` in the Wanted with substitution [a :-> Int], we can
  add a derived FunDepEqns
     FDEqns{ fd_qtvs = [], fd_eqs = [ [Int] ~ alpha ] }
@@ -1119,7 +1128,7 @@ instance are bound by the pre-unification step.  Suppose we have
     [W] F alpha ~ [ty]
 -Then, the RHS [G a] pre-unifies with the RHS of the Wanted, but with an
 +Then, the RHS [G a] pre-matches with the RHS of the Wanted, but with an
  empty substitution, which does not fix `a`.  So we get this FunDepEqns:
     FDEqns{ fd_qtvs = a, fd_eqs = [ Maybe a ~ alpha ] }
  (note the fd_qtvs=a) and thereby emit (via `instantiateFunDepEqns`)
@@ -1133,36 +1142,44 @@ In general we have:
    type instance forall qs. F t1 ... tn = rhs
    [W] F a1 ... an ~ b
 -Suppose `b` pre-unifies with `rhs`, with substitution `S` that binds
 -some (but perhaps not all) of the `qs`.  Lets say
 -   unbound_qs = qs \ dom(S)
+-
 -Then we generate the FunDepEqs
 -   FDEqns{ fd_qtvs = unbound_qs
 -         , fd_eqs = [ S(t1) ~ S(a1), S(t3) ~ S(a3) ]
+-
 -These 'fd_qtvs' are subsequently instantiated to fresh metavariables by
 -'instantiateFunDepEqns'.
+-
 -(OF1) The computation of `unbound_qs` is done by `trim_qtvs`, but we
 -   have to be careful.   Suppose (OF1a)
 -       qs = [ k::*, a::k ]
 -       S  = [ k :-> UnliftedType ]
 -   Then we want
 -       unbound_qs = [ a::UnliftedType ]    -- Must apply S to q's kind!!
+-
 -   And (OF1b), although I'm not sure if this can acutally 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` is 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
 +Suppose `b` pre-matches with `rhs`, with substitution `S`.  We /ignore/
 +`S` and simply generate the FunDepEqs
 +   FDEqns{ fd_qtvs = qs, fd_eqs = [ t1 ~ a1, t3 ~ a3 ]
 +These 'fd_qtvs' are subsequently instantiated to fresh meta-variables by
 +'instantiateFunDepEqns'.  See Historical Note [trim_qtvs].
++
 +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.
  Note [Exploiting closed type families] see `mkTopClosedFamEqFDs`
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1194,9 +1211,6 @@ More precisely, here is the very clever Closed Family Fundep Algorithm (CFFA)
      with fresh unification vars in lhs and rhs for the quantified variables of the
      equation.
 -    Actually we take advantage of the substitution generated by the relevance
 -    check, see (CF7) below.
+-
  See Note [Relevance] for what "relevant" means.
  We need to take care about non-termination; see (CF3).
@@ -1391,26 +1405,59 @@ Key point: equations that are not relevant do not need to be considered for fund
  (CF7) Relevance.  When computing relevance in the Closed Family Fundep Algorithm,
    for [W] F wlhs1 wlhs2 ~ wrhs, against an equation   F lhs1 lhs2 ~ rhs
    we get back a pre-unifying substitution S that makes the two as equal as poss.
 -  Then we use `trim_qtvs` in exactly the same way as in
 -       (OF1) of Note [Exploiting open type families], to generate qtvs' and S'
 -  Then we generate
 -      FDEqns { fd_qtvs = qtvs', fd_eqs [ S'(lhs1) ~ wlhs1
 -                                       , S'(lhs2) ~ wlhs2
 -                                       , S'(rhs)  ~ wrhs ] }
 -  Notice that we do /not/ apply S' to wlhs/wrhs.  These type contain unification
 -  variables that we must actually unify! Example
 +  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
       type family F a b where
         F [a] (Maybe b) = (a,  G b)
       [W] F alpha beta ~ (Int, [gamma])
    Pre-unification gives [alpha :-> [a], beta :-> Maybe b, a :-> Int]
 -  This substitution eliminates the quantified variable `a` but not `b`, so we
 -  want this:
 -     FDEqns { fd_qtvs = [b], fd_eqs [ [Int] ~ alpha
 -                                    , Maybe b ~ beta
 -                                    , (Int,G b) ~ (Int, [gamma]) ] }
+-
 -  Notice also that by applying the substitution to the template but not to the
 -  Wanted, we uphold the `fd_eqs` invariant in `FDEqns` (see its data type decl)
 +  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).
  Note [Cache-caused loops]
  ~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1517,8 +1564,8 @@ instantiateFunDepEqns (FDEqns { fd_qtvs = qtvs, fd_eqs = eqs })
      rev_eqs = reverse eqs
         -- (reverse eqs): See Note [Reverse order of fundep equations]
 -    -- The kinds of `qtvs` can have free variables, because of `trim_qtvs`
 -    -- Example: T27828b
 +    -- The kinds of `qtvs` can have free variables;
 +    -- in the FDEqns produced by GHC.Tc.Instance.FunDeps.improveFromInstEnv
      empty_subst = mkEmptySubst $ mkInScopeSet $
                    tyCoVarsOfTypes (map tyVarKind qtvs)

testsuite/tests/typecheck/should_compile/T27994.hs

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

testsuite/tests/typecheck/should_compile/T27994a.hs

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

testsuite/tests/typecheck/should_compile/all.T

@@ -972,4 +972,6 @@ test('T27557', normal, compile, [''])
  test('T27664', normal, compile, [''])
  test('T27916', normal, compile, [''])
  test('T26543_orig', normal, compile, [''])
 +test('T27994',  normal, compile, [''])
 +test('T27994a', normal, compile, [''])