[Git][ghc/ghc][wip/T22194-flags] More bug fixes

Simon Peyton Jones (@simonpj) gitlab at gitlab.haskell.org
Wed Mar 15 08:17:28 UTC 2023



Simon Peyton Jones pushed to branch wip/T22194-flags at Glasgow Haskell Compiler / GHC


Commits:
7dcf3659 by Simon Peyton Jones at 2023-03-14T23:53:09+00:00
More bug fixes

- - - - -


5 changed files:

- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/Unify.hs


Changes:

=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -847,8 +847,9 @@ injectiveVarsOfType look_under_tfs = go
     go CoercionTy{}                 = emptyFV
 
     go_tc tc tys
-      | isFamilyTyCon tc
-      = if | look_under_tfs, Injective flags <- tyConInjectivityInfo tc
+      | isTypeFamilyTyCon tc
+      = if | look_under_tfs
+           , Injective flags <- tyConInjectivityInfo tc
            -> mapUnionFV go $
               filterByList (flags ++ repeat True) tys
                          -- Oversaturated arguments to a tycon are


=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -634,8 +634,8 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2
        ; let redn1 = mkReduction co1 ty1'
 
        ; new_ev <- rewriteEqEvidence emptyRewriterSet ev' swapped
-                     redn1
-                     (mkReflRedn Representational ps_ty2)
+                     redn1 (mkReflRedn Representational ps_ty2)
+
        ; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
 
 ---------
@@ -1713,18 +1713,29 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
   , TyVarLHS tv <- lhs
   = do { given_eq_lvl <- getInnermostGivenEqLevel
        ; if not (touchabilityTest given_eq_lvl tv rhs)
-         then canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
+         then if | Just can_rhs <- canTyFamEqLHS_maybe rhs
+                 -> swapAndFinish ev eq_rel swapped tv can_rhs
+                 | otherwise
+                 -> canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
          else
 
     -- We have a touchable unification variable on the left
     do { check_result <- checkTouchableTyVarEq ev tv rhs
        ; case check_result of {
-            PuFail reason -> cantMakeCanonical reason ev eq_rel swapped lhs rhs ;
-            PuOK redn _   ->
+            PuFail reason
+               | Just can_rhs <- canTyFamEqLHS_maybe rhs
+               -> swapAndFinish ev eq_rel swapped tv can_rhs
+               | otherwise
+               -> tryIrredInstead reason ev eq_rel swapped lhs rhs ;
+
+            PuOK rhs_redn _ ->
 
     -- Success: we can solve by unification
-    do { let tv_ty     = mkTyVarTy tv
-             final_rhs = reductionReducedType redn
+    do { new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
+                       (mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn
+
+       ; let tv_ty     = mkTyVarTy tv
+             final_rhs = reductionReducedType rhs_redn
              tv_lvl    = tcTyVarLevel tv
 
        ; traceTcS "Sneaky unification:" $
@@ -1738,7 +1749,7 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
 
        -- Provide Refl evidence for the constraint
        -- Ignore 'swapped' because it's Refl!
-       ; setEvBindIfWanted ev IsCoherent $
+       ; setEvBindIfWanted new_ev IsCoherent $
          evCoercion (mkNomReflCo final_rhs)
 
        -- Set the unification flag if we have done outer unifications
@@ -1750,15 +1761,15 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
        -- Kick out any constraints that can now be rewritten
        ; n_kicked <- kickOutAfterUnification tv
 
-       ; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) }}}}
+       ; return (Stop new_ev (text "Solved by unification" <+> pprKicked n_kicked)) }}}}
 
   -- Otherwise unification is off the table
   | otherwise
   = canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
 
-
 ---------------------------
 -- Unification is off the table
+-- Here we never have TyVarLHS ~ TyFamLHS (it is always the other way)
 canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
   = do { -- Do checkTypeEq to guarantee (TyEq:OC), (TyEq:F)
          -- Must do the occurs check even on tyvar/tyvar equalities,
@@ -1766,7 +1777,7 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
        ; check_result <- checkTypeEq ev eq_rel lhs rhs
 
        ; case check_result of {
-            PuFail reason   -> cantMakeCanonical reason ev eq_rel swapped lhs rhs ;
+            PuFail reason   -> tryIrredInstead reason ev eq_rel swapped lhs rhs ;
             PuOK rhs_redn _ ->
 
     do { new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
@@ -1777,29 +1788,30 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
                           , eq_rhs = reductionReducedType rhs_redn }) }}}
 
 ----------------------
-cantMakeCanonical :: CheckTyEqResult -> CtEvidence -> EqRel -> SwapFlag
-                  -> CanEqLHS -> TcType
-                  -> TcS (StopOrContinue Ct)
-cantMakeCanonical reason ev eq_rel swapped lhs rhs
-  | TyVarLHS tv <- lhs
-  , Just (tc,tys) <- splitTyConApp_maybe rhs
-  , isFamilyTyCon tc
-  , let lhs_ty = mkTyVarTy tv
-  = -- Flip (a ~ F tys) to (F tys ~ a)
-    do { new_ev <- rewriteEqEvidence emptyRewriterSet ev (flipSwap swapped)
-                           (mkReflRedn role rhs) (mkReflRedn role lhs_ty)
+swapAndFinish :: CtEvidence -> EqRel -> SwapFlag
+              -> TcTyVar -> CanEqLHS      -- a ~ F tys
+              -> TcS (StopOrContinue Ct)
+-- We have an equality a ~ F tys, and want to flip it to
+-- (F tys ~ a), whereupon it is canonical
+swapAndFinish ev eq_rel swapped lhs_tv can_rhs
+  = do { let lhs_ty = mkTyVarTy lhs_tv
+       ; new_ev <- rewriteEqEvidence emptyRewriterSet ev (flipSwap swapped)
+                       (mkReflRedn role (canEqLHSType can_rhs))
+                       (mkReflRedn role lhs_ty)
        ; interactEq (EqCt { eq_ev  = new_ev, eq_eq_rel = eq_rel
-                          , eq_lhs = TyFamLHS tc tys
-                          , eq_rhs = lhs_ty }) }
-
-  | otherwise
-  = do { traceTcS "cantMakeCanonical" (ppr lhs $$ ppr rhs)
-       ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
-                           (mkReflRedn role (canEqLHSType lhs)) (mkReflRedn role rhs)
-       ; solveIrredEquality (NonCanonicalReason reason) new_ev }
+                          , eq_lhs = can_rhs, eq_rhs = lhs_ty }) }
   where
     role = eqRelRole eq_rel
 
+----------------------
+tryIrredInstead :: CheckTyEqResult -> CtEvidence -> EqRel -> SwapFlag
+                -> CanEqLHS -> TcType -> TcS (StopOrContinue Ct)
+-- We have a non-canonical equality
+-- No need to swap; just hand it off
+tryIrredInstead reason ev _eq_rel _swapped lhs rhs
+  = do { traceTcS "cantMakeCanonical" (ppr reason $$ ppr lhs $$ ppr rhs)
+       ; solveIrredEquality (NonCanonicalReason reason) ev }
+
 -----------------------
 -- | Solve a reflexive equality constraint
 canEqReflexive :: CtEvidence    -- ty ~ ty


=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -2073,33 +2073,34 @@ checkTouchableTyVarEq
 --   with extra wanteds 'cts'
 -- If it returns (PuFail reason) we can't unify, and the reason explains why.
 checkTouchableTyVarEq ev lhs_tv rhs
-  = do { traceTcS "checkTouchableTyVarEq" (ppr lhs_tv $$ ppr rhs)
-       ; check_result <- wrapTcS check_rhs
-       ; traceTcS "checkTouchableTyVarEq 2" (ppr lhs_tv $$ ppr check_result)
+  = do { traceTcS "checkTouchableTyVarEq {" (ppr lhs_tv $$ ppr rhs)
+       ; check_result <- wrapTcS (check_rhs rhs)
+       ; traceTcS "checkTouchableTyVarEq }" (ppr lhs_tv $$ ppr check_result)
        ; case check_result of
             PuFail reason -> return (PuFail reason)
             PuOK redn cts -> do { emitWork (bagToList cts)
                                 ; return (pure redn) } }
   where
-    check_rhs = case splitTyConApp_maybe rhs of
-      Just (tc, tys) | isTypeFamilyTyCon tc
-                     , not (isConcreteTyVar lhs_tv)
-        -> -- Crucial special case for  alpha ~ F tys
-           -- We don't want to flatten that (F tys)!
-           do { tys_res <- mapCheck (checkTyEqRhs simple_flags) tys
-              ; return (mkTyConAppRedn Nominal tc <$> tys_res) }
+    check_rhs rhs
+       -- Crucial special case for  alpha ~ F tys
+       -- We don't want to flatten that (F tys)!
+       | Just (tc,tys) <- splitTyConApp_maybe rhs
+       , isTypeFamilyTyCon tc
+       , not (isConcreteTyVar lhs_tv)
+       = do { tys_res <- mapCheck (checkTyEqRhs arg_flags) tys
+            ; return (mkTyConAppRedn Nominal tc <$> tys_res) }
 
-      -- Normal case
-      _other -> checkTyEqRhs flags rhs
+       | otherwise = checkTyEqRhs flags rhs
 
     flags | MetaTv { mtv_info = tv_info, mtv_tclvl = tv_lvl } <- tcTyVarDetails lhs_tv
           = TEF { tef_foralls  = isRuntimeUnkSkol lhs_tv
                 , tef_fam_app  = mkTEFA_Break ev (break_wanted tv_lvl)
                 , tef_unifying = Unifying tv_info tv_lvl LC_Promote
-                , tef_lhs      = TyVarLHS lhs_tv }
+                , tef_lhs      = TyVarLHS lhs_tv
+                , tef_occurs   = cteInsolubleOccurs }
           | otherwise = pprPanic "checkTouchableTyVarEq" (ppr lhs_tv)
 
-    simple_flags = stopPromoting flags
+    arg_flags = famAppArgFlags flags
 
     break_wanted lhs_tv_lvl fam_app   -- Occurs check or skolem escape; so flatten
       = do { new_tv_ty <- TcM.newMetaTyVarTyAtLevel lhs_tv_lvl (typeKind fam_app)
@@ -2125,7 +2126,10 @@ checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType
 -- For Wanteds, don't bother
 checkTypeEq ev eq_rel lhs rhs
   | isGiven ev
-  = do { check_result <- wrapTcS (checkTyEqRhs given_flags rhs)
+  = do { traceTcS "checkTypeEq {" (vcat [ text "lhs:" <+> ppr lhs
+                                        , text "rhs:" <+> ppr rhs ])
+       ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs)
+       ; traceTcS "checkTypeEq }" (ppr check_result)
        ; case check_result of
             PuFail reason -> return (PuFail reason)
             PuOK redn prs -> do { let prs_list = bagToList prs
@@ -2143,19 +2147,25 @@ checkTypeEq ev eq_rel lhs rhs
   where
     given_flags = TEF { tef_lhs      = lhs
                       , tef_foralls  = False
-                      , tef_unifying = NotUnifying eq_rel
-                      , tef_fam_app  = mkTEFA_Break ev break_given }
+                      , tef_unifying = NotUnifying
+                      , tef_fam_app  = mkTEFA_Break ev break_given
+                      , tef_occurs   = occ_prob }
         -- TEFA_Break used for: [G] a ~ Maybe (F a)
         --                   or [W] F a ~ Maybe (F a)
 
     wanted_flags = TEF { tef_lhs      = lhs
                        , tef_foralls  = False
-                       , tef_unifying = NotUnifying eq_rel
-                       , tef_fam_app  = TEFA_Recurse }
+                       , tef_unifying = NotUnifying
+                       , tef_fam_app  = TEFA_Recurse
+                       , tef_occurs   = occ_prob }
         -- TEFA_Recurse: no point in TEFA_Break, because we would just make
         --      [W] beta[tau] ~ F ty (beta fresh)
         -- and would then unify beta in the next step. Infinite loop!
 
+    occ_prob = case eq_rel of
+                 NomEq  -> cteInsolubleOccurs
+                 ReprEq -> cteSolubleOccurs
+
     break_given :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
     break_given fam_app
       = do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app)


=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -43,8 +43,8 @@ module GHC.Tc.Types.Constraint (
         cterHasNoProblem, cterHasProblem, cterHasOnlyProblem,
         cterRemoveProblem, cterHasOccursCheck, cterFromKind,
 
-        CanEqLHS(..), canEqLHS_maybe, canEqLHSKind, canEqLHSType,
-        eqCanEqLHS,
+        CanEqLHS(..), canEqLHS_maybe, canTyFamEqLHS_maybe,
+        canEqLHSKind, canEqLHSType, eqCanEqLHS,
 
         Hole(..), HoleSort(..), isOutOfScopeHole,
         DelayedError(..), NotConcreteError(..),
@@ -761,6 +761,11 @@ canEqLHS_maybe xi
   | Just tv <- getTyVar_maybe xi
   = Just $ TyVarLHS tv
 
+  | otherwise
+  = canTyFamEqLHS_maybe xi
+
+canTyFamEqLHS_maybe :: Xi -> Maybe CanEqLHS
+canTyFamEqLHS_maybe xi
   | Just (tc, args) <- tcSplitTyConApp_maybe xi
   , isTypeFamilyTyCon tc
   , args `lengthIs` tyConArity tc


=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -36,7 +36,7 @@ module GHC.Tc.Utils.Unify (
   checkTyEqRhs,
   PuResult(..), failCheckWith, okCheckRefl, mapCheck,
   TyEqFlags(..), TyEqFamApp(..), AreUnifying(..), LevelCheck(..), FamAppBreaker,
-  stopPromoting, occursCheckTv
+  famAppArgFlags, occursCheckTv
   ) where
 
 import GHC.Prelude
@@ -63,7 +63,6 @@ import GHC.Core.TyCon
 import GHC.Core.Coercion
 import GHC.Core.Multiplicity
 import GHC.Core.Reduction
-import GHC.Core.Predicate( EqRel(..) )
 
 import qualified GHC.LanguageExtensions as LangExt
 
@@ -2542,7 +2541,8 @@ uTypeCheckTouchableTyVarEq lhs_tv rhs
           = TEF { tef_foralls  = False
                 , tef_fam_app  = TEFA_Fail
                 , tef_unifying = Unifying tv_info tv_lvl LC_None
-                , tef_lhs      = TyVarLHS lhs_tv }
+                , tef_lhs      = TyVarLHS lhs_tv
+                , tef_occurs   = cteInsolubleOccurs }
           | otherwise
           = pprPanic "uTypeCheckTouchableTyVarEq" (ppr lhs_tv)
           -- TEFA_Fail: See Note [Prevent unification with type families]
@@ -2692,7 +2692,8 @@ data TyEqFlags a
   = TEF { tef_foralls  :: Bool         -- Allow foralls
         , tef_lhs      :: CanEqLHS     -- LHS of the constraint
         , tef_unifying :: AreUnifying  -- Always NotUnifying if tef_lhs is TyFamLHS
-        , tef_fam_app  :: TyEqFamApp a }
+        , tef_fam_app  :: TyEqFamApp a
+        , tef_occurs   :: CheckTyEqProblem }  -- Soluble or insoluble occurs check
 
 -- What to do for a type-family application
 data TyEqFamApp a
@@ -2708,7 +2709,6 @@ data AreUnifying
        LevelCheck
 
   | NotUnifying         -- Not attempting to unify
-       EqRel            -- Role of equality (unifying is always NomEq)
 
 data LevelCheck
   = LC_None       -- Level check not needed: we should never encounter a
@@ -2719,17 +2719,20 @@ data LevelCheck
   | LC_Promote    -- Do a level check against this level; if it fails on a
                   --  unification variable, promote it
 
-stopPromoting :: TyEqFlags a -> TyEqFlags a
+famAppArgFlags :: TyEqFlags a -> TyEqFlags a
+-- Adjust the flags when going undter a type family
 -- Only the outer family application gets the loop-breaker treatment
 -- Ditto tyvar promotion.  E.g.
 --        [W] alpha[2] ~ Maybe (F beta[3])
 -- Do not promote beta[3]; instead promote (F beta[3])
-stopPromoting flags@(TEF { tef_unifying = unifying })
-  = flags { tef_fam_app = TEFA_Recurse, tef_unifying = unifying' }
+famAppArgFlags flags@(TEF { tef_unifying = unifying })
+  = flags { tef_fam_app  = TEFA_Recurse
+          , tef_unifying = zap_promotion unifying
+          , tef_occurs   = cteSolubleOccurs }
+            -- tef_occurs: under a type family, an occurs check is not definitely-insoluble
   where
-    unifying' = case unifying of
-                  Unifying info lvl LC_Promote -> Unifying info lvl LC_Check
-                  _                            -> unifying
+    zap_promotion (Unifying info lvl LC_Promote) = Unifying info lvl LC_Check
+    zap_promotion unifying                       = unifying
 
 type FamAppBreaker a = TcType -> TcM (PuResult a Reduction)
      -- Given a family-application ty, return a Reduction :: ty ~ cvb
@@ -2777,7 +2780,9 @@ checkCo :: TyEqFlags a -> Coercion -> TcM (PuResult a Coercion)
 checkCo (TEF { tef_lhs = TyFamLHS {} }) co
   = return (PuOK co emptyBag)
 
-checkCo (TEF { tef_lhs = TyVarLHS lhs_tv, tef_unifying = unifying }) co
+checkCo (TEF { tef_lhs = TyVarLHS lhs_tv
+             , tef_unifying = unifying
+             , tef_occurs = occ_prob }) co
   -- Check for coercion holes, if unifying
   -- See (COERCION-HOLE) in Note [Unification preconditions]
   | Unifying {} <- unifying
@@ -2786,14 +2791,14 @@ checkCo (TEF { tef_lhs = TyVarLHS lhs_tv, tef_unifying = unifying }) co
 
   -- Occurs check (can promote)
   | Unifying _ lhs_tv_lvl LC_Promote <- unifying
-  = do { reason <- checkFreeVars lhs_tv lhs_tv_lvl (tyCoVarsOfCo co)
+  = do { reason <- checkFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfCo co)
        ; if cterHasNoProblem reason
          then return (pure co)
          else failCheckWith reason }
 
   -- Occurs check (no promotion)
   | lhs_tv `elemVarSet` tyCoVarsOfCo co
-  = failCheckWith insolubleOccursProblem
+  = failCheckWith (cteProblem occ_prob)
 
   | otherwise
   = return (PuOK co emptyBag)
@@ -2831,51 +2836,52 @@ checkTyConApp flags tc_app tc tys
 checkFamApp :: TyEqFlags a
             -> TcType -> TyCon -> [TcType]  -- Saturated family application
             -> TcM (PuResult a Reduction)
-checkFamApp flags fam_app tc tys
-  | Unifying lhs_info _ _ <- tef_unifying flags
+checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob
+                       , tef_fam_app = fam_app_flag, tef_lhs = lhs })
+            fam_app tc tys
+  | Unifying lhs_info _ _ <- unifying
   , isConcreteInfo lhs_info
   = failCheckWith (cteProblem cteConcrete)
 
   | otherwise
-  = case tef_fam_app flags of
+  = case fam_app_flag of
       TEFA_Fail    -> failCheckWith (cteProblem cteTypeFamily)
 
       TEFA_Recurse
-        | TyFamLHS lhs_tc lhs_tys <- tef_lhs flags
+        | TyFamLHS lhs_tc lhs_tys <- lhs
         , tcEqTyConApps lhs_tc lhs_tys tc tys
-        , let eq_rel = case tef_unifying flags of
-                         Unifying {}        -> NomEq
-                         NotUnifying eq_rel -> eq_rel
-        -> failCheckWith (occursProblem eq_rel)
+        -> failCheckWith (cteProblem occ_prob)
 
         | otherwise
-        -> do { tys_res <- mapCheck (checkTyEqRhs flags) tys
+        -> do { tys_res <- mapCheck (checkTyEqRhs arg_flags) tys
               ; return (mkTyConAppRedn Nominal tc <$> tys_res) }
 
       TEFA_Break breaker
-        | TyFamLHS lhs_tc lhs_tys <- tef_lhs flags
+        | TyFamLHS lhs_tc lhs_tys <- lhs
         , tcEqTyConApps lhs_tc lhs_tys tc tys
         -> breaker fam_app
         | otherwise
-        -> do { tys_res <- mapCheck (checkTyEqRhs (stopPromoting flags)) tys
+        -> do { tys_res <- mapCheck (checkTyEqRhs arg_flags) tys
               ; case tys_res of
                   PuOK redns cts -> return (PuOK (mkTyConAppRedn Nominal tc redns) cts)
                   PuFail {}      -> breaker fam_app }
+  where
+    arg_flags = famAppArgFlags flags
 
 -------------------
 checkTyVar :: forall a. TyEqFlags a -> TcTyVar -> TcM (PuResult a Reduction)
-checkTyVar flags occ_tv
-  = case tef_lhs flags of
+checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob }) occ_tv
+  = case lhs of
       TyFamLHS {}     -> success   -- Nothing to do if the LHS is a type-family
-      TyVarLHS lhs_tv -> check_tv (tef_unifying flags) lhs_tv
+      TyVarLHS lhs_tv -> check_tv unifying lhs_tv
   where
     lvl_occ = tcTyVarLevel occ_tv
     success = okCheckRefl (mkTyVarTy occ_tv)
 
     ---------------------
-    check_tv (NotUnifying eq_rel) lhs_tv
+    check_tv NotUnifying lhs_tv
       | occursCheckTv lhs_tv occ_tv
-      = failCheckWith (occursProblem eq_rel)
+      = failCheckWith (cteProblem occ_prob)
       | otherwise
       = success
 
@@ -2893,7 +2899,7 @@ checkTyVar flags occ_tv
                -> TcTyVar -> TcM (PuResult a Reduction)
     check_unif lhs_tv_info lhs_tv_lvl prom lhs_tv
       | lhs_tv == occ_tv  -- We check the kind of occ_tv later, in checkFreeVars
-      = failCheckWith insolubleOccursProblem
+      = failCheckWith (cteProblem occ_prob)
 
       | isConcreteInfo lhs_tv_info
       , not (isConcreteTyVar occ_tv)
@@ -2929,7 +2935,7 @@ checkTyVar flags occ_tv
                  new_lvl = lhs_tv_lvl `minTcLevel` lvl_occ
                            -- c[conc,3] ~ p[tau,2]: want to clone p:=p'[conc,2]
                            -- c[tau,2]  ~ p[tau,3]: want to clone p:=p'[tau,2]
-           ; reason <- checkFreeVars lhs_tv lhs_tv_lvl (tyCoVarsOfType (tyVarKind occ_tv))
+           ; reason <- checkFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfType (tyVarKind occ_tv))
            ; if cterHasNoProblem reason  -- Successfully promoted
              then do { new_tv_ty <- promote_meta_tyvar new_info new_lvl occ_tv
                      ; okCheckRefl new_tv_ty }
@@ -2937,17 +2943,19 @@ checkTyVar flags occ_tv
       | otherwise = pprPanic "promote" (ppr occ_tv)
 
 -------------------------
-checkFreeVars :: TcTyVar -> TcLevel -> TyCoVarSet -> TcM CheckTyEqResult
+checkFreeVars :: CheckTyEqProblem    -- Occurs check problem
+              -> TcTyVar -> TcLevel
+              -> TyCoVarSet -> TcM CheckTyEqResult
 -- Check this set of TyCoVars for
 --   (a) occurs check
 --   (b) promote if necessary, or report skolem escape
-checkFreeVars lhs_tv lhs_tv_lvl vs
+checkFreeVars occ_prob lhs_tv lhs_tv_lvl vs
   = do { oks <- mapM do_one (nonDetEltsUniqSet vs)
        ; return (mconcat oks) }
   where
     do_one :: TyCoVar -> TcM CheckTyEqResult
     do_one v | isCoVar v           = return cteOK
-             | lhs_tv == v         = return insolubleOccursProblem
+             | lhs_tv == v         = return (cteProblem occ_prob)
              | no_promotion        = return cteOK
              | not (isMetaTyVar v) = return (cteProblem cteSkolemEscape)
              | otherwise           = promote_one v



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7dcf3659e1338d0819eaca026c88bf4990485251

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7dcf3659e1338d0819eaca026c88bf4990485251
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230315/15e3d41f/attachment-0001.html>


More information about the ghc-commits mailing list