[Git][ghc/ghc][wip/T25657] More wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Sun Mar 2 23:26:45 UTC 2025
Simon Peyton Jones pushed to branch wip/T25657 at Glasgow Haskell Compiler / GHC
Commits:
c9ca52c9 by Simon Peyton Jones at 2025-03-02T23:26:16+00:00
More wibbles
- - - - -
4 changed files:
- compiler/GHC/Core/Predicate.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Core/Predicate.hs
=====================================
@@ -30,7 +30,11 @@ module GHC.Core.Predicate (
isIPPred_maybe,
-- Evidence variables
- DictId, isEvVar, isDictId
+ DictId, isEvVar, isDictId,
+
+ -- Equality left-hand sides
+ CanEqLHS(..), canEqLHS_maybe, canTyFamEqLHS_maybe,
+ canEqLHSKind, canEqLHSType, eqCanEqLHS,
) where
@@ -38,7 +42,7 @@ import GHC.Prelude
import GHC.Core.Type
import GHC.Core.Class
-import GHC.Core.TyCo.Compare( eqType )
+import GHC.Core.TyCo.Compare( eqType, tcEqTyConApps )
import GHC.Core.TyCon
import GHC.Core.TyCon.RecWalk
import GHC.Types.Var
@@ -52,6 +56,13 @@ import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Data.FastString
+
+{- *********************************************************************
+* *
+* Pred and PredType *
+* *
+********************************************************************* -}
+
-- | A predicate in the solver. The solver tries to prove Wanted predicates
-- from Given ones.
data Pred
@@ -229,9 +240,12 @@ predTypeEqRel ty
| isReprEqPred ty = ReprEq
| otherwise = NomEq
-{-------------------------------------------
-Predicates on PredType
---------------------------------------------}
+
+{- *********************************************************************
+* *
+* Predicates on PredType *
+* *
+********************************************************************* -}
{-
Note [Evidence for quantified constraints]
@@ -492,3 +506,61 @@ isEvVar var = isEvVarType (varType var)
isDictId :: Id -> Bool
isDictId id = isDictTy (varType id)
+
+
+{- *********************************************************************
+* *
+* Equality left-hand sides
+* *
+********************************************************************* -}
+
+-- | A 'CanEqLHS' is a type that can appear on the left of a canonical
+-- equality: a type variable or /exactly-saturated/ type family application.
+data CanEqLHS
+ = TyVarLHS TyVar
+ | TyFamLHS TyCon -- ^ TyCon of the family
+ [Type] -- ^ Arguments, /exactly saturating/ the family
+
+instance Outputable CanEqLHS where
+ ppr (TyVarLHS tv) = ppr tv
+ ppr (TyFamLHS fam_tc fam_args) = ppr (mkTyConApp fam_tc fam_args)
+
+-----------------------------------
+-- | Is a type a canonical LHS? That is, is it a tyvar or an exactly-saturated
+-- type family application?
+-- Does not look through type synonyms.
+canEqLHS_maybe :: Type -> Maybe CanEqLHS
+canEqLHS_maybe xi
+ | Just tv <- getTyVar_maybe xi
+ = Just $ TyVarLHS tv
+
+ | otherwise
+ = canTyFamEqLHS_maybe xi
+
+canTyFamEqLHS_maybe :: Type -> Maybe CanEqLHS
+canTyFamEqLHS_maybe xi
+ | Just (tc, args) <- tcSplitTyConApp_maybe xi
+ , isTypeFamilyTyCon tc
+ , args `lengthIs` tyConArity tc
+ = Just $ TyFamLHS tc args
+
+ | otherwise
+ = Nothing
+
+-- | Convert a 'CanEqLHS' back into a 'Type'
+canEqLHSType :: CanEqLHS -> Type
+canEqLHSType (TyVarLHS tv) = mkTyVarTy tv
+canEqLHSType (TyFamLHS fam_tc fam_args) = mkTyConApp fam_tc fam_args
+
+-- | Retrieve the kind of a 'CanEqLHS'
+canEqLHSKind :: CanEqLHS -> Kind
+canEqLHSKind (TyVarLHS tv) = tyVarKind tv
+canEqLHSKind (TyFamLHS fam_tc fam_args) = piResultTys (tyConKind fam_tc) fam_args
+
+-- | Are two 'CanEqLHS's equal?
+eqCanEqLHS :: CanEqLHS -> CanEqLHS -> Bool
+eqCanEqLHS (TyVarLHS tv1) (TyVarLHS tv2) = tv1 == tv2
+eqCanEqLHS (TyFamLHS fam_tc1 fam_args1) (TyFamLHS fam_tc2 fam_args2)
+ = tcEqTyConApps fam_tc1 fam_args1 fam_tc2 fam_args2
+eqCanEqLHS _ _ = False
+
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -35,9 +35,10 @@ import GHC.Builtin.Names( tYPETyConKey, cONSTRAINTTyConKey )
import GHC.Core.Type hiding ( getTvSubstEnv )
import GHC.Core.Coercion hiding ( getCvSubstEnv )
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 )
+import GHC.Core.TyCo.Compare ( eqType, tcEqType, tcEqTyConApps )
import GHC.Core.TyCo.FVs ( tyCoVarsOfCoList, tyCoFVsOfTypes )
import GHC.Core.TyCo.Subst ( mkTvSubst )
import GHC.Core.Map.Type
@@ -46,7 +47,7 @@ import GHC.Core.Multiplicity
import GHC.Utils.FV( FV, fvVarList )
import GHC.Utils.Misc
import GHC.Utils.Outputable
-import GHC.Types.Basic( SwapFlag(..), isSwapped )
+import GHC.Types.Basic( SwapFlag(..) )
import GHC.Types.Unique.FM
import GHC.Exts( oneShot )
import GHC.Utils.Panic
@@ -655,7 +656,7 @@ tcUnifyTyForInjectivity
tcUnifyTyForInjectivity unif in_scope t1 t2
= case tc_unify_tys alwaysBindFam alwaysBindTv
unif -- Am I unifying?
- True -- Do injetivity checks
+ True -- Do injectivity checks
False -- Don't check outermost kinds
RespectMultiplicities
rn_env emptyTvSubstEnv emptyCvSubstEnv
@@ -1432,12 +1433,12 @@ unify_ty env (CoercionTy co1) (CoercionTy co2) kco
_ -> return () }
-unify_ty env ty1@(TyVarTy {}) ty2 kco
- = uVarOrFam env ty1 ty2 kco
+unify_ty env (TyVarTy tv1) ty2 kco
+ = uVarOrFam env (TyVarLHS tv1) ty2 kco
-unify_ty env ty1 ty2@(TyVarTy {}) kco
+unify_ty env ty1 (TyVarTy tv2) kco
| um_unif env -- If unifying, can swap args; but not when matching
- = uVarOrFam (umSwapRn env) ty2 ty1 (mkSymCo kco)
+ = uVarOrFam (umSwapRn env) (TyVarLHS tv2) ty1 (mkSymCo kco)
-- Deal with TyConApps
unify_ty env ty1 ty2 kco
@@ -1460,12 +1461,12 @@ unify_ty env ty1 ty2 kco
; unless (um_inj_tf env) $ -- See (end of) Note [Specification of unification]
don'tBeSoSure MARTypeFamily $ unify_tys env noninj_tys1 noninj_tys2 }
- | Just {} <- mb_sat_fam_app1
- = uVarOrFam env ty1 ty2 kco
+ | Just (tc,tys) <- mb_sat_fam_app1
+ = uVarOrFam env (TyFamLHS tc tys) ty2 kco
| um_unif env
- , Just {} <- mb_sat_fam_app2
- = uVarOrFam (umSwapRn env) ty2 ty1 (mkSymCo kco)
+ , Just (tc,tys) <- mb_sat_fam_app2
+ = uVarOrFam (umSwapRn env) (TyFamLHS tc tys) ty1 (mkSymCo kco)
-- Handle oversaturated type families. Suppose we have
-- (F a b) ~ (c d) where F has arity 1
@@ -1594,9 +1595,10 @@ isSatFamApp (TyConApp tc tys)
isSatFamApp _ = Nothing
---------------------------------
-uVarOrFam :: UMEnv -> InType -> InType -> OutCoercion -> UM ()
+uVarOrFam :: UMEnv -> CanEqLHS -> InType -> OutCoercion -> UM ()
-- Invariants: (a) ty1 is a TyVarTy or a saturated type-family application
-- (b) If ty1 is a ty-fam-app, then ty2 is NOT a TyVarTy
+-- (c) both args have had coreView already applied
-- Why saturated? See (ATF4) in Note [Apartness and type families]
uVarOrFam env ty1 ty2 kco
= do { substs <- getSubstEnvs
@@ -1609,18 +1611,11 @@ uVarOrFam env ty1 ty2 kco
-- E.g. a ~ F p q
-- Starts with: go a (F p q)
-- if `a` not bindable, swap to: go (F p q) a
- go swapped substs (TyVarTy tv1) ty2 kco
+ go swapped substs (TyVarLHS tv1) ty2 kco
= go_tv swapped substs tv1 ty2 kco
- go swapped substs ty1 ty2 kco
- | Just (tc,tys) <- isSatFamApp ty1
- = go_fam swapped substs ty1 tc tys ty2 kco
-
- go swapped _ ty1 ty2 _
- = assertPpr (isSwapped swapped) (ppr ty1 $$ ppr ty2) $
- -- NB: uVarOrFam calls `go` with ty1=tyvar/tyfaapp,
- -- but `go` may recurse having swapped
- surelyApart
+ go swapped substs (TyFamLHS tc tys) ty2 kco
+ = go_fam swapped substs tc tys ty2 kco
-----------------------------
-- go_tv: LHS is a type variable
@@ -1663,12 +1658,13 @@ uVarOrFam env ty1 ty2 kco
extendTvEnv tv1' rhs -- Bind tv1:=rhs and continue
-- When unifying, try swapping:
- -- e.g. a ~ F p q we might succeed with go_fam
- -- e.g. a ~ beta we might be able to bind `beta` but not `a`
+ -- e.g. a ~ F p q with `a` not bindable: we might succeed with go_fam
+ -- e.g. a ~ beta with `a` not bindable: we might be able to bind `beta`
-- e.g. beta ~ F beta Int occurs check; but MaybeApart after swapping
| um_unif env
, NotSwapped <- swapped -- If we have swapped already, don't do so again
- = go IsSwapped substs ty2 ty1 (mkSymCo kco)
+ , Just lhs2 <- canEqLHS_maybe ty2
+ = go IsSwapped substs lhs2 (mkTyVarTy tv1) (mkSymCo kco)
| occurs_check = maybeApart MARInfinite -- Occurs check
| otherwise = surelyApart
@@ -1694,27 +1690,28 @@ uVarOrFam env ty1 ty2 kco
-----------------------------
-- go_fam: LHS is a saturated type-family application
-- Invariant: ty2 is not a TyVarTy
- go_fam swapped substs ty1 tc tys1 ty2 kco
+ go_fam swapped substs tc1 tys1 ty2 kco
-- If we are under a forall, just give up and return MaybeApart
-- see (ATF3) in Note [Apartness and type families]
| not (isEmptyVarSet (um_foralls env))
= maybeApart MARTypeFamily
-- We are not under any foralls, so the RnEnv2 is empty
- | Just ty1' <- lookupFamEnv (um_fam_env substs) tc tys1
+ | Just ty1' <- lookupFamEnv (um_fam_env substs) tc1 tys1
= if | um_unif env -> unify_ty env ty1' ty2 kco
| (ty1' `mkCastTy` kco) `tcEqType` ty2 -> maybeApart MARTypeFamily
| otherwise -> surelyApart
-- Check for equality F tys ~ F tys
-- otherwise we'd build an infinite substitution
- | ty1 `tcEqType` rhs
+ | TyConApp tc2 tys2 <- ty2
+ , tcEqTyConApps tc1 tys1 tc2 tys2
= return ()
-- Now check if we can bind the (F tys) to the RHS
- | BindMe <- um_bind_fam_fun env tc tys1 rhs
+ | BindMe <- um_bind_fam_fun env tc1 tys1 rhs
= -- ToDo: do we need an occurs check here?
- do { extendFamEnv tc tys1 rhs
+ do { extendFamEnv tc1 tys1 rhs
; maybeApart MARTypeFamily }
-- Swap in case of (F a b) ~ (G c d e)
@@ -1723,7 +1720,8 @@ uVarOrFam env ty1 ty2 kco
-- see (ATF6) in Note [Apartness and type families]
| um_unif env
, NotSwapped <- swapped
- = go IsSwapped substs ty2 ty1 (mkSymCo kco)
+ , Just lhs2 <- canEqLHS_maybe ty2
+ = go IsSwapped substs lhs2 (mkTyConApp tc1 tys1) (mkSymCo kco)
| otherwise -- See (ATF4) in Note [Apartness and type families]
= surelyApart
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -47,9 +47,6 @@ module GHC.Tc.Types.Constraint (
cterRemoveProblem, cterHasOccursCheck, cterFromKind,
- CanEqLHS(..), canEqLHS_maybe, canTyFamEqLHS_maybe,
- canEqLHSKind, canEqLHSType, eqCanEqLHS,
-
Hole(..), HoleSort(..), isOutOfScopeHole,
DelayedError(..), NotConcreteError(..),
@@ -286,17 +283,6 @@ data EqCt -- An equality constraint; see Note [Canonical equalities]
eq_eq_rel :: EqRel -- INVARIANT: cc_eq_rel = ctEvEqRel cc_ev
}
--- | A 'CanEqLHS' is a type that can appear on the left of a canonical
--- equality: a type variable or /exactly-saturated/ type family application.
-data CanEqLHS
- = TyVarLHS TcTyVar
- | TyFamLHS TyCon -- ^ TyCon of the family
- [Xi] -- ^ Arguments, /exactly saturating/ the family
-
-instance Outputable CanEqLHS where
- ppr (TyVarLHS tv) = ppr tv
- ppr (TyFamLHS fam_tc fam_args) = ppr (mkTyConApp fam_tc fam_args)
-
eqCtEvidence :: EqCt -> CtEvidence
eqCtEvidence = eq_ev
@@ -777,45 +763,6 @@ instance Outputable Ct where
instance Outputable EqCt where
ppr (EqCt { eq_ev = ev }) = ppr ev
------------------------------------
--- | Is a type a canonical LHS? That is, is it a tyvar or an exactly-saturated
--- type family application?
--- Does not look through type synonyms.
-canEqLHS_maybe :: Xi -> Maybe CanEqLHS
-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
- = Just $ TyFamLHS tc args
-
- | otherwise
- = Nothing
-
--- | Convert a 'CanEqLHS' back into a 'Type'
-canEqLHSType :: CanEqLHS -> TcType
-canEqLHSType (TyVarLHS tv) = mkTyVarTy tv
-canEqLHSType (TyFamLHS fam_tc fam_args) = mkTyConApp fam_tc fam_args
-
--- | Retrieve the kind of a 'CanEqLHS'
-canEqLHSKind :: CanEqLHS -> TcKind
-canEqLHSKind (TyVarLHS tv) = tyVarKind tv
-canEqLHSKind (TyFamLHS fam_tc fam_args) = piResultTys (tyConKind fam_tc) fam_args
-
--- | Are two 'CanEqLHS's equal?
-eqCanEqLHS :: CanEqLHS -> CanEqLHS -> Bool
-eqCanEqLHS (TyVarLHS tv1) (TyVarLHS tv2) = tv1 == tv2
-eqCanEqLHS (TyFamLHS fam_tc1 fam_args1) (TyFamLHS fam_tc2 fam_args2)
- = tcEqTyConApps fam_tc1 fam_args1 fam_tc2 fam_args2
-eqCanEqLHS _ _ = False
-
{-
************************************************************************
* *
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -88,7 +88,7 @@ import GHC.Core.TyCo.Ppr( debugPprType {- pprTyVar -} )
import GHC.Core.TyCon
import GHC.Core.Coercion
import GHC.Core.Unify
-import GHC.Core.Predicate( EqRel(..), mkEqPredRole, mkNomEqPred )
+import GHC.Core.Predicate( EqRel(..), CanEqLHS(..), mkEqPredRole, mkNomEqPred )
import GHC.Core.Multiplicity
import GHC.Core.Reduction
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c9ca52c97724c8c7f1d1be2fdc96502dbfe2da8e
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c9ca52c97724c8c7f1d1be2fdc96502dbfe2da8e
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/20250302/04373e63/attachment-0001.html>
More information about the ghc-commits
mailing list