GitLab

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

Commits:

0f5ff61c
by Simon Peyton Jones at 2026-09-27T17:31:10+01:00
```
Further wibbles
```

26bd3aa5

by Simon Peyton Jones at 2026-09-27T18:37:50+01:00

More wibbles

...incl a new assert in the _no_unification case

4 changed files:

compiler/GHC/Tc/Solver/Equality.hs
compiler/GHC/Tc/Solver/Monad.hs
compiler/GHC/Tc/Utils/Unify.hs
testsuite/tests/indexed-types/should_fail/T9662.stderr

Changes:

compiler/GHC/Tc/Solver/Equality.hs

@@ -1824,7 +1824,7 @@ Ticket #10009, a very nasty example:
      g :: forall a. (UnF (F a) ~ a) => a -> ()
      g _ = f (undefined :: F a)
 -For g we get [G]  g1 : UnF (F a) ~ a
 +For g we get [G] g1 : UnF (F a) ~ a
               [W] w1 : UnF (F beta) ~ beta
               [W] w2 : F a ~ F beta
@@ -2213,6 +2213,9 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
                -- We have a touchable unification variable on the left,
                -- and the top-shape check succeeded. These are both guaranteed
                -- by the fact that simpleUnifyCheck did not return SUC_CannotUnify.
 +              --
 +              -- Next, do a fully `checkTyEqRhs` check to see if we can unify
 +              -- See Note [checkTyEqRhs] in GHC.Tc.Utils.Unify
                do  { let flags = unifyingLHSMetaTyVar_TEFTask ev lhs_tv
                    ; check_result <- wrapTcS (checkTyEqRhs flags rhs)
                    ; traceTcS "canEqCanLHSFinish_try_unification" $
@@ -2229,21 +2232,19 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
    = finish_no_unify
    where
 -    -- We can't unify, but we can see if this equality can go in the inert set
 -    -- and be used to rewrite other constraints.
 -    finish_no_unify = canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
+-
 -    -- We can't unify, and this equality should not be used to rewrite
 -    -- other constraints (e.g. because it has an occurs check).
 -    -- So add it to the inert Irreds.
 ---    try_irred reason = tryIrredInstead reason ev eq_rel swapped lhs rhs
+-
 -    -- We can't unify as-is, and want to flip the equality around.
 -    -- Example: alpha ~ F tys, flip it around to become the canonical
 -    -- equality f tys ~ alpha.
 ---    swap_and_finish tv can_rhs = swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs
 +    -- finish_no_unify: abandon the attempt to unify, and instead hand off to
 +    -- canEqCanLHSFinish_no_unification
 +    -- First, though, if we have (tv ~ F tys)
 +    --        swap it over so we get (F tys ~ tv), with `F tys` on the LHS
 +    -- See Note [Orienting TyVarLHS/TyFamLHS]
 +    finish_no_unify
 +      | TyVarLHS lhs_tv <- lhs
 +      , Just can_rhs <- canTyFamEqLHS_maybe rhs
 +      = canEqCanLHSFinish_no_unification ev eq_rel (flipSwap swapped) can_rhs (mkTyVarTy lhs_tv)
 +      | otherwise
 +      = canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
 -    -- Phew! Finally!  We can unify; go ahead and do so.
 +    -- do_unification: Phew! Finally!  We can unify; go ahead and do so.
      do_unification tv rhs_redn =
        do { -- In the common case where rhs_redn is Refl, we don't need to rewrite
             -- the evidence, even if swapped=IsSwapped.   Suppose the original was
@@ -2280,39 +2281,41 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
           ; return (Stop new_ev (text "Solved by unification")) }
  ---------------------------
 --- Unification is off the table
  canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
 +  -- We can't unify, but we can see if this equality can go in the inert set
 +  -- and be used to rewrite other constraints.
 +  -- See Note [Equalities where unification fails]
    = do { -- Do checkTypeEq to guarantee (TyEq:OC), (TyEq:F)
           -- Must do the occurs check even on tyvar/tyvar equalities,
           -- in case have  x ~ (y :: ..x...); this is #12593.
         ; check_result <- checkTypeEq ev eq_rel lhs rhs
+-
 -       ; let lhs_ty = canEqLHSType lhs
         ; case check_result of
              PuFail reason
+-
 -              -- If we had F a ~ G (F a), which gives an occurs check,
 -              -- then swap it to G (F a) ~ F a, which does not
 -              -- See Note [Orienting TyVarLHS/TyFamLHS]
 -              -- ToDo: fix me  ... also needed for a ~ G (F a)
 -              -- However `swap_for_size` above will orient it with (G (F a)) on
 -              -- the left anwyway.  `swap_for_rewriting` "wins", but that doesn't
 -              -- matter: in the occurs check case swap_for_rewriting will be moot.
 -              -- TL;DR: the next four lines of code are redundant
 -              -- I'm leaving them here in case they become relevant again
 -              | Just can_rhs <- canTyFamEqLHS_maybe rhs
 -              , reason `cterHasOnlyProblem` cteSolubleOccurs
 -              -> finishWith ev eq_rel (flipSwap swapped) can_rhs lhs_ty
+-
                | reason `cterHasOnlyProblems` do_not_prevent_rewriting
 -              -> finishWith ev eq_rel swapped lhs rhs
 +              ->   do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs
 +                      ; continueWith $ Right $
 +                        EqCt { eq_ev  = new_ev, eq_eq_rel = eq_rel
 +                             , eq_lhs = lhs , eq_rhs = rhs } }
                | otherwise
 -              -> tryIrredInstead reason ev eq_rel swapped lhs rhs
 +              -> -- We can't unify, and this equality should not be used to rewrite
 +                 -- other constraints (e.g. because it has an occurs check).
 +                 -- So add it to the inert Irreds.
 +                 do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs
 +                    ; finishCanWithIrred (NonCanonicalReason reason) new_ev }
              PuOK new_eqs rhs_redn
 -              -> do { emitWork new_eqs
 +              -> -- Claim: there should be no new_eqs
 +                 -- The non-unification check does non promotion nor type-family
 +                 -- flattening for Wanteds
 +                 assertPpr (isEmptyCts new_eqs)
 +                    (vcat [ text "new_eqs"  <+> ppr new_eqs
 +                          , text "rhs_redn" <+> ppr rhs_redn
 +                          , text "lhs"      <+> ppr lhs
 +                          , text "rhs"      <+> ppr rhs ]) $
 +                 do { emitWork new_eqs
                      ; let new_holes = rewriterSetFromCts new_eqs
 +                          lhs_ty    = canEqLHSType lhs
                            lhs_redn  = mkReflRedn (eqRelRole eq_rel) lhs_ty
                      ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn new_holes
@@ -2336,45 +2339,7 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
  do_not_prevent_rewriting :: CheckTyEqResult
  do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<>
                             cteProblem cteConcrete
+-
 -----------------------
 -finishWith :: CtEvidence -> EqRel -> SwapFlag
 -           -> CanEqLHS -> TcType
 -           -> TcS (StopOrContinue (Either unused EqCt))
 -finishWith ev eq_rel swapped can_lhs rhs_ty
 -  = do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped can_lhs rhs_ty
 -       ; continueWith $ Right $
 -         EqCt { eq_ev  = new_ev, eq_eq_rel = eq_rel
 -              , eq_lhs = can_lhs , eq_rhs = rhs_ty } }
+-
 -{-
 -swapAndFinish :: CtEvidence -> EqRel -> SwapFlag
 -              -> TcType -> CanEqLHS      -- ty ~ F tys
 -              -> TcS (StopOrContinue (Either unused EqCt))
 --- We have an equality alpha ~ F tys, that we can't unify e.g because 'tys'
 --- mentions alpha, it would not be a canonical constraint as-is.
 --- We want to flip it to (F tys ~ a), whereupon it is canonical
 -swapAndFinish ev eq_rel swapped lhs_ty can_rhs
 -  = do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel (flipSwap swapped) can_rhs lhs_ty
 -       ; continueWith $ Right $
 -         EqCt { eq_ev  = new_ev, eq_eq_rel = eq_rel
 -              , eq_lhs = can_rhs, eq_rhs = lhs_ty } }
 --}
+-
  ----------------------
 -tryIrredInstead :: CheckTyEqResult -> CtEvidence
 -                -> EqRel -> SwapFlag -> CanEqLHS -> TcType
 -                -> TcS (StopOrContinue (Either IrredCt unused))
 --- We have a non-canonical equality
 --- We still swap it if 'swapped' says so, so that it is oriented
 --- in the direction that the error-reporting machinery
 --- expects it; e.g.  (m ~ t m) rather than (t m ~ m)
 --- This is not very important, and only affects error reporting.
 -tryIrredInstead reason ev eq_rel swapped lhs rhs
 -  = do { traceTcS "cantMakeCanonical" (ppr reason $$ ppr lhs $$ ppr rhs)
 -       ; new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs
 -       ; finishCanWithIrred (NonCanonicalReason reason) new_ev }
+-
  finishCanWithIrred :: CtIrredReason -> CtEvidence
                     -> TcS (StopOrContinue (Either IrredCt a))
  finishCanWithIrred reason ev
@@ -2394,8 +2359,26 @@ canEqReflexive ev eq_rel ty
    = do { setEqIfWanted ev (mkReflCPH eq_rel ty)
         ; stopWith ev "Solved by reflexivity" }
 -{- Note [Equalities with heterogeneous kinds]
 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 +{- Note [Equalities where unification fails]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 +If we can't unify, but the equality is canonical, we still want to add it to the
 +inert set so that it can be used to rewrite other Wanteds.  (There are many
 +reasons by unification might not happen: the LHS is not a touchable unification
 +variable, it has rewriters, it's a Given etc.)
++
 +* In this case we call `checkTypeEq`to see if it is canonical (which in turn
 +  calls `checkTypeEqRhs`).
++
 +* Even if `checkTypeEq` returns `PuFail`, we may /still/ be able to add it to the inert
 +  set, depending on the reason for failure; examples are given in `do_not_prevent_rewriting`.
++
 +* NB: we do /not/ try to take advantage of the case where `canEqCanLHSFinish_try_unification`
 +  has already called `checkTyEqRhs`; doing so caused #27844.   (The first call did fam-app
 +  breaking, which concealed a genuine occurs check.)  It's just too clever; better to do
 +  the simple thing.
++
 +Note [Equalities with heterogeneous kinds]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  What do we do when we have an equality
    (tv :: k1) ~ (rhs :: k2)
@@ -3066,8 +3049,6 @@ inertsEqsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w
  inertsEqsCanDischarge _ _ = Nothing
+-
+-
  {- Note [Do not unify Givens]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Consider this GADT match
@@ -3133,34 +3114,6 @@ Wrinkles:
     we should kick out `co` so that we can now unify it, which might
     unlock other stuff.  See `kickOutAfterFillingCoercionHole` in
     GHC.Tc.Solver.Monad.
+-
 -Note [Solve by unification]
 -~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -If we solve
 -   alpha[n] ~ ty
 -by unification, there are two cases to consider
+-
 -* TouchableSameLevel: if the ambient level is 'n', then
 -  we can simply update alpha := ty, and do nothing else
+-
 -* TouchableOuterLevel free_metas n: if the ambient level is greater than
 -  'n' (the level of alpha), in addition to setting alpha := ty we must
 -  do two other things:
+-
 -  1. Promote all the free meta-vars of 'ty' to level n.  After all,
 -     alpha[n] is at level n, and so if we set, say,
 -          alpha[n] := Maybe beta[m],
 -     we must ensure that when unifying beta we do skolem-escape checks
 -     etc relevant to level n.  Simple way to do that: promote beta to
 -     level n.
+-
 -  2. Set the Unification Level Flag to record that a level-n unification has
 -     taken place. See Note [WhatUnifications] in GHC.Tc.Utils.Unify
+-
 -NB: TouchableSameLevel is just an optimisation for TouchableOuterLevel. Promotion
 -would be a no-op, and setting the unification flag unnecessarily would just
 -make the solver iterate more often.  (We don't need to iterate when unifying
 -at the ambient level because of the kick-out mechanism.)
  -}

compiler/GHC/Tc/Solver/Monad.hs

@@ -2333,7 +2333,7 @@ checkTypeEq ev eq_rel lhs rhs =
      given_flags :: TyEqFlags TcM (TcTyVar, TcType)
      given_flags = wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven }
          -- TEFA_Break used for: [G] a ~ Maybe (F a)
 -        --                   or [W] F a ~ Maybe (F a)
 +        --                   or [G] F a ~ Maybe (F a)
      -- occ_prob: see Note [Occurs check and representational equality]
      occ_prob = case eq_rel of

compiler/GHC/Tc/Utils/Unify.hs

@@ -4203,7 +4203,7 @@ famAppArgFlags flags = case flags of
  The key function `checkTyEqRhs ty_eq_flags rhs` is called on the
  RHS of a type equality
         lhs ~ rhs
 -and checks to see if `rhs` satisfies, or can be made to satisfy,
 +and checks to see if `rhs` satisfies, /or can be made to satisfy/,
  invariants described by `ty_eq_flags`.  It can succeded or fail; in
  the latter case it returns a `CheckTyEqResult` that describes why it
  failed.
@@ -4224,6 +4224,15 @@ Notably, it can check for things like:
    * Concreteness error
        e.g. alpha[conc] ~ r[sk]
 +Note "or can be made to satisfy the preconditions"!  `checkTyEqRhs` may transform
 +the RHS by
++
 +  * Turning a type-family application into a type variable, perhaps to avoid
 +    an occurs check.  See Note Note [Family applications in canonical constraints]
++
 +  * Promoting any nested unification variables, in order to satisfy the
 +    level invariant. See Note [Promotion and level-checking]
++
  Its specific behaviour is governed by the `TyEqFlags` that are passed
  to it; see Note [TyEqFlags].

testsuite/tests/indexed-types/should_fail/T9662.stderr

  T9662.hs:49:8: error: [GHC-25897]
 -    • Couldn't match type ‘n’ with ‘Int’
 +    • Couldn't match type ‘m’ with ‘Int’
        Expected: Exp (((sh :. k) :. m) :. n)
                  -> Exp (((sh :. m) :. n) :. k)
          Actual: Exp
                    (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
                  -> Exp
                       (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))
 -      ‘n’ is a rigid type variable bound by
 +      ‘m’ is a rigid type variable bound by
          the type signature for:
            test :: forall sh k m n.
                    Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)