diff options
author | sheaf <sam.derbyshire@gmail.com> | 2022-03-02 00:12:17 +0100 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2022-03-02 14:08:36 -0500 |
commit | b27b2af3fab48e21aabcc9441967c4dd7a6a75ea (patch) | |
tree | ca2919f3d98c35b6a22b08118ca32f4dae04a40d /compiler/GHC/Tc/Utils/TcType.hs | |
parent | aeea6bd588060108dea88996c19f48b9e50adad2 (diff) | |
download | haskell-b27b2af3fab48e21aabcc9441967c4dd7a6a75ea.tar.gz |
Introduce ConcreteTv metavariables
This patch introduces a new kind of metavariable, by adding the
constructor `ConcreteTv` to `MetaInfo`. A metavariable with
`ConcreteTv` `MetaInfo`, henceforth a concrete metavariable, can only
be unified with a type that is concrete (that is, a type that answers
`True` to `GHC.Core.Type.isConcrete`).
This solves the problem of dangling metavariables in `Concrete#`
constraints: instead of emitting `Concrete# ty`, which contains a
secret existential metavariable, we simply emit a primitive equality
constraint `ty ~# concrete_tv` where `concrete_tv` is a fresh concrete
metavariable.
This means we can avoid all the complexity of canonicalising
`Concrete#` constraints, as we can just re-use the existing machinery
for `~#`.
To finish things up, this patch then removes the `Concrete#` special
predicate, and instead introduces the special predicate `IsRefl#`
which enforces that a coercion is reflexive.
Such a constraint is needed because the canonicaliser is quite happy
to rewrite an equality constraint such as `ty ~# concrete_tv`, but
such a rewriting is not handled by the rest of the compiler currently,
as we need to make use of the resulting coercion, as outlined in the
FixedRuntimeRep plan.
The big upside of this approach (on top of simplifying the code)
is that we can now selectively implement PHASE 2 of FixedRuntimeRep,
by changing individual calls of `hasFixedRuntimeRep_MustBeRefl` to
`hasFixedRuntimeRep` and making use of the obtained coercion.
Diffstat (limited to 'compiler/GHC/Tc/Utils/TcType.hs')
-rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 30 |
1 files changed, 26 insertions, 4 deletions
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 807ad0ab56..b01f72b185 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -41,6 +41,7 @@ module GHC.Tc.Utils.TcType ( MetaDetails(Flexi, Indirect), MetaInfo(..), skolemSkolInfo, isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy, tcIsTcTyVar, isTyVarTyVar, isOverlappableTyVar, isTyConableTyVar, + isConcreteTyVar, isAmbiguousTyVar, isCycleBreakerTyVar, metaTyVarRef, metaTyVarInfo, isFlexi, isIndirect, isRuntimeUnkSkol, metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe, @@ -566,21 +567,27 @@ data MetaDetails | Indirect TcType data MetaInfo - = TauTv -- This MetaTv is an ordinary unification variable + = TauTv -- ^ This MetaTv is an ordinary unification variable -- A TauTv is always filled in with a tau-type, which -- never contains any ForAlls. - | TyVarTv -- A variant of TauTv, except that it should not be + | TyVarTv -- ^ A variant of TauTv, except that it should not be -- unified with a type, only with a type variable -- See Note [TyVarTv] in GHC.Tc.Utils.TcMType - | RuntimeUnkTv -- A unification variable used in the GHCi debugger. + | RuntimeUnkTv -- ^ A unification variable used in the GHCi debugger. -- It /is/ allowed to unify with a polytype, unlike TauTv | CycleBreakerTv -- Used to fix occurs-check problems in Givens -- See Note [Type variable cycles] in -- GHC.Tc.Solver.Canonical + | ConcreteTv + -- ^ A unification variable that can only be unified + -- with a concrete type, in the sense of + -- Note [Concrete types] in GHC.Tc.Utils.Concrete. + -- See Note [ConcreteTv] in GHC.Tc.Utils.Concrete. + instance Outputable MetaDetails where ppr Flexi = text "Flexi" ppr (Indirect ty) = text "Indirect" <+> ppr ty @@ -590,6 +597,7 @@ instance Outputable MetaInfo where ppr TyVarTv = text "tyv" ppr RuntimeUnkTv = text "rutv" ppr CycleBreakerTv = text "cbv" + ppr ConcreteTv = text "conc" {- ********************************************************************* * * @@ -1081,6 +1089,18 @@ isCycleBreakerTyVar tv | otherwise = False +-- | Is this type variable a concrete type variable, i.e. +-- it is a metavariable with 'ConcreteTv' 'MetaInfo'? +-- +-- Works with both 'TyVar' and 'TcTyVar'. +isConcreteTyVar :: TcTyVar -> Bool +isConcreteTyVar tv + | isTcTyVar tv + , MetaTv { mtv_info = ConcreteTv } <- tcTyVarDetails tv + = True + | otherwise + = False + isMetaTyVarTy :: TcType -> Bool isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv isMetaTyVarTy _ = False @@ -1892,7 +1912,9 @@ isImprovementPred ty ClassPred cls _ -> classHasFds cls IrredPred {} -> True -- Might have equalities after reduction? ForAllPred {} -> False - SpecialPred {} -> False + SpecialPred s -> + case s of + IsReflPrimPred {} -> False {- Note [Expanding superclasses] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |