summaryrefslogtreecommitdiff
path: root/compiler/GHC/Core
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/GHC/Core')
-rw-r--r--compiler/GHC/Core/Coercion.hs30
-rw-r--r--compiler/GHC/Core/Predicate.hs16
-rw-r--r--compiler/GHC/Core/TyCo/FVs.hs9
-rw-r--r--compiler/GHC/Core/TyCo/Rep.hs42
-rw-r--r--compiler/GHC/Core/Type.hs2
5 files changed, 67 insertions, 32 deletions
diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index ef6d4af5ec..22f3c32201 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -122,8 +122,7 @@ module GHC.Core.Coercion (
multToCo,
- hasCoercionHoleTy, hasCoercionHoleCo,
- HoleSet, coercionHolesOfType, coercionHolesOfCo,
+ hasCoercionHoleTy, hasCoercionHoleCo, hasThisCoercionHoleTy,
setCoHoleType
) where
@@ -156,7 +155,6 @@ import GHC.Builtin.Types.Prim
import GHC.Data.List.SetOps
import GHC.Data.Maybe
import GHC.Types.Unique.FM
-import GHC.Types.Unique.Set
import GHC.Utils.Misc
import GHC.Utils.Outputable
@@ -2725,16 +2723,13 @@ has_co_hole_co :: Coercion -> Monoid.Any
(has_co_hole_ty, _, has_co_hole_co, _)
= foldTyCo folder ()
where
- folder = TyCoFolder { tcf_view = const Nothing
+ folder = TyCoFolder { tcf_view = noView
, tcf_tyvar = const2 (Monoid.Any False)
, tcf_covar = const2 (Monoid.Any False)
, tcf_hole = const2 (Monoid.Any True)
, tcf_tycobinder = const2
}
- const2 :: a -> b -> c -> a
- const2 x _ _ = x
-
-- | Is there a coercion hole in this type?
hasCoercionHoleTy :: Type -> Bool
hasCoercionHoleTy = Monoid.getAny . has_co_hole_ty
@@ -2743,19 +2738,16 @@ hasCoercionHoleTy = Monoid.getAny . has_co_hole_ty
hasCoercionHoleCo :: Coercion -> Bool
hasCoercionHoleCo = Monoid.getAny . has_co_hole_co
--- | A set of 'CoercionHole's
-type HoleSet = UniqSet CoercionHole
-
--- | Extract out all the coercion holes from a given type
-coercionHolesOfType :: Type -> UniqSet CoercionHole
-coercionHolesOfCo :: Coercion -> UniqSet CoercionHole
-(coercionHolesOfType, _, coercionHolesOfCo, _) = foldTyCo folder ()
+hasThisCoercionHoleTy :: Type -> CoercionHole -> Bool
+hasThisCoercionHoleTy ty hole = Monoid.getAny (f ty)
where
- folder = TyCoFolder { tcf_view = const Nothing -- don't look through synonyms
- , tcf_tyvar = \ _ _ -> mempty
- , tcf_covar = \ _ _ -> mempty
- , tcf_hole = const unitUniqSet
- , tcf_tycobinder = \ _ _ _ -> ()
+ (f, _, _, _) = foldTyCo folder ()
+
+ folder = TyCoFolder { tcf_view = noView
+ , tcf_tyvar = const2 (Monoid.Any False)
+ , tcf_covar = const2 (Monoid.Any False)
+ , tcf_hole = \ _ h -> Monoid.Any (getUnique h == getUnique hole)
+ , tcf_tycobinder = const2
}
-- | Set the type of a 'CoercionHole'
diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs
index bf6d10f0f7..3de166364b 100644
--- a/compiler/GHC/Core/Predicate.hs
+++ b/compiler/GHC/Core/Predicate.hs
@@ -30,6 +30,7 @@ module GHC.Core.Predicate (
-- Implicit parameters
isIPLikePred, hasIPSuperClasses, isIPTyCon, isIPClass,
isCallStackTy, isCallStackPred, isCallStackPredTy,
+ isIPPred_maybe,
-- Evidence variables
DictId, isEvVar, isDictId
@@ -51,7 +52,9 @@ import GHC.Builtin.Types.Prim ( concretePrimTyCon )
import GHC.Utils.Outputable
import GHC.Utils.Misc
import GHC.Utils.Panic
-import GHC.Data.FastString( FastString )
+import GHC.Data.FastString
+
+import Control.Monad ( guard )
-- | A predicate in the solver. The solver tries to prove Wanted predicates
@@ -351,6 +354,15 @@ isCallStackTy ty
= False
+-- | Decomposes a predicate if it is an implicit parameter. Does not look in
+-- superclasses. See also [Local implicit parameters].
+isIPPred_maybe :: Type -> Maybe (FastString, Type)
+isIPPred_maybe ty =
+ do (tc,[t1,t2]) <- splitTyConApp_maybe ty
+ guard (isIPTyCon tc)
+ x <- isStrLitTy t1
+ return (x,t2)
+
{- Note [Local implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The function isIPLikePred tells if this predicate, or any of its
@@ -380,7 +392,7 @@ Several wrinkles
instantiate and check each superclass, one by one, in
hasIPSuperClasses.
-* With -XRecursiveSuperClasses, the superclass hunt can go on forever,
+* With -XUndecidableSuperClasses, the superclass hunt can go on forever,
so we need a RecTcChecker to cut it off.
* Another apparent additional complexity involves type families. For
diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs
index 28929f37f9..e837132fc0 100644
--- a/compiler/GHC/Core/TyCo/FVs.hs
+++ b/compiler/GHC/Core/TyCo/FVs.hs
@@ -265,9 +265,6 @@ runTyCoVars :: Endo TyCoVarSet -> TyCoVarSet
{-# INLINE runTyCoVars #-}
runTyCoVars f = appEndo f emptyVarSet
-noView :: Type -> Maybe Type
-noView _ = Nothing
-
{- *********************************************************************
* *
Deep free variables
@@ -382,8 +379,8 @@ shallowTcvFolder = TyCoFolder { tcf_view = noView
********************************************************************* -}
-{- Note [Finding free coercion varibles]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Finding free coercion variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Here we are only interested in the free /coercion/ variables.
We can achieve this through a slightly different TyCo folder.
@@ -392,6 +389,7 @@ Notice that we look deeply, into kinds.
See #14880.
-}
+-- See Note [Finding free coercion variables]
coVarsOfType :: Type -> CoVarSet
coVarsOfTypes :: [Type] -> CoVarSet
coVarsOfCo :: Coercion -> CoVarSet
@@ -432,7 +430,6 @@ deepCoVarFolder = TyCoFolder { tcf_view = noView
-- See Note [CoercionHoles and coercion free variables]
-- in GHC.Core.TyCo.Rep
-
{- *********************************************************************
* *
Closing over kinds
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index fae7c7de19..a08da28421 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -65,7 +65,7 @@ module GHC.Core.TyCo.Rep (
pickLR,
-- ** Analyzing types
- TyCoFolder(..), foldTyCo,
+ TyCoFolder(..), foldTyCo, noView,
-- * Sizes
typeSize, coercionSize, provSize,
@@ -150,6 +150,7 @@ data Type
| ForAllTy
{-# UNPACK #-} !TyCoVarBinder
Type -- ^ A Π type.
+ -- Note [When we quantify over a coercion variable]
-- INVARIANT: If the binder is a coercion variable, it must
-- be mentioned in the Type. See
-- Note [Unused coercion variable in ForAllTy]
@@ -624,6 +625,35 @@ In order to compare FunTys while respecting how they could
expand into TyConApps, we must check
the kinds of the arg and the res.
+Note [When we quantify over a coercion variable]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The TyCoVarBinder in a ForAllTy can be (most often) a TyVar or (rarely)
+a CoVar. We support quantifying over a CoVar here in order to support
+a homogeneous (~#) relation (someday -- not yet implemented). Here is
+the example:
+
+ type (:~~:) :: forall k1 k2. k1 -> k2 -> Type
+ data a :~~: b where
+ HRefl :: a :~~: a
+
+Assuming homogeneous equality (that is, with
+ (~#) :: forall k. k -> k -> TYPE (TupleRep '[])
+) after rejigging to make equalities explicit, we get a constructor that
+looks like
+
+ HRefl :: forall k1 k2 (a :: k1) (b :: k2).
+ forall (cv :: k1 ~# k2). (a |> cv) ~# b
+ => (:~~:) k1 k2 a b
+
+Note that we must cast `a` by a cv bound in the same type in order to
+make this work out.
+
+See also https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell/phase2
+which gives a general road map that covers this space.
+
+Having this feature in Core does *not* mean we have it in source Haskell.
+See #15710 about that.
+
Note [Unused coercion variable in ForAllTy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
@@ -1834,7 +1864,7 @@ We were also worried about
`extendVarSet` tv
Here deep_fvs and deep_tcf are mutually recursive, unlike fvs and tcf.
-But, amazingly, we get good code here too. GHC is careful not to makr
+But, amazingly, we get good code here too. GHC is careful not to mark
TyCoFolder data constructor for deep_tcf as a loop breaker, so the
record selections still cancel. And eta expansion still happens too.
-}
@@ -1843,8 +1873,8 @@ data TyCoFolder env a
= TyCoFolder
{ tcf_view :: Type -> Maybe Type -- Optional "view" function
-- E.g. expand synonyms
- , tcf_tyvar :: env -> TyVar -> a
- , tcf_covar :: env -> CoVar -> a
+ , tcf_tyvar :: env -> TyVar -> a -- Does not automatically recur
+ , tcf_covar :: env -> CoVar -> a -- into kinds of variables
, tcf_hole :: env -> CoercionHole -> a
-- ^ What to do with coercion holes.
-- See Note [Coercion holes] in "GHC.Core.TyCo.Rep".
@@ -1916,6 +1946,10 @@ foldTyCo (TyCoFolder { tcf_view = view
go_prov _ (PluginProv _) = mempty
go_prov _ (CorePrepProv _) = mempty
+-- | A view function that looks through nothing.
+noView :: Type -> Maybe Type
+noView _ = Nothing
+
{- *********************************************************************
* *
typeSize, coercionSize
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 1cacfca468..4fce8c8a09 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -86,7 +86,7 @@ module GHC.Core.Type (
-- ** Analyzing types
TyCoMapper(..), mapTyCo, mapTyCoX,
- TyCoFolder(..), foldTyCo,
+ TyCoFolder(..), foldTyCo, noView,
-- (Newtypes)
newTyConInstRhs,
View Lorry Controller Status