Commit 0faf7fd3 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Refactor the treatment of predicate types

Trac #15648 showed that GHC was a bit confused about the
difference between the types for

* Predicates
* Coercions
* Evidence (in the typechecker constraint solver)

This patch cleans it up. See especially Type.hs
Note [Types for coercions, predicates, and evidence]

Particular changes

* Coercion types (a ~# b) and (a ~#R b) are not predicate types
  (so isPredTy reports False for them) and are not implicitly
  instantiated by the type checker.  This is a real change, but
  it consistently reflects that fact that (~#) and (~R#) really
  are different from predicates.

* isCoercionType is renamed to isCoVarType

* During type inference, simplifyInfer, we do /not/ want to infer
  a constraint (a ~# b), because that is no longer a predicate type.
  So we 'lift' it to (a ~ b). See TcType
  Note [Lift equality constaints when quantifying]

* During type inference for pattern synonyms, we need to 'lift'
  provided constraints of type (a ~# b) to (a ~ b).  See
  Note [Equality evidence in pattern synonyms] in PatSyn

* But what about (forall a. Eq a => a ~# b)? Is that a
  predicate type?  No -- it does not have kind Constraint.
  Is it an evidence type?  Perhaps, but awkwardly so.

  In the end I decided NOT to make it an evidence type,
  and to ensure the the type inference engine never
  meets it.  This made me /simplify/ the code in
  TcCanonical.makeSuperClasses; see TcCanonical
  Note [Equality superclasses in quantified constraints]

  Instead I moved the special treatment for primitive
  equality to TcInteract.doTopReactOther.  See TcInteract
  Note [Looking up primitive equalities in quantified constraints]

  Also see Note [Evidence for quantified constraints] in Type.

  All this means I can have
     isEvVarType ty = isCoVarType ty || isPredTy ty
  which is nice.

All in all, rather a lot of work for a small refactoring,
but I think it's a real improvement.
parent 321bc1a6
......@@ -267,20 +267,20 @@ mkVanillaGlobalWithInfo = mkGlobalId VanillaId
-- | For an explanation of global vs. local 'Id's, see "Var#globalvslocal"
mkLocalId :: Name -> Type -> Id
mkLocalId name ty = mkLocalIdWithInfo name ty vanillaIdInfo
-- It's tempting to ASSERT( not (isCoercionType ty) ), but don't. Sometimes,
-- It's tempting to ASSERT( not (isCoVarType ty) ), but don't. Sometimes,
-- the type is a panic. (Search invented_id)
-- | Make a local CoVar
mkLocalCoVar :: Name -> Type -> CoVar
mkLocalCoVar name ty
= ASSERT( isCoercionType ty )
= ASSERT( isCoVarType ty )
Var.mkLocalVar CoVarId name ty vanillaIdInfo
-- | Like 'mkLocalId', but checks the type to see if it should make a covar
mkLocalIdOrCoVar :: Name -> Type -> Id
mkLocalIdOrCoVar name ty
| isCoercionType ty = mkLocalCoVar name ty
| otherwise = mkLocalId name ty
| isCoVarType ty = mkLocalCoVar name ty
| otherwise = mkLocalId name ty
-- | Make a local id, with the IdDetails set to CoVarId if the type indicates
-- so.
......@@ -288,8 +288,8 @@ mkLocalIdOrCoVarWithInfo :: Name -> Type -> IdInfo -> Id
mkLocalIdOrCoVarWithInfo name ty info
= Var.mkLocalVar details name ty info
where
details | isCoercionType ty = CoVarId
| otherwise = VanillaId
details | isCoVarType ty = CoVarId
| otherwise = VanillaId
-- proper ids only; no covars!
mkLocalIdWithInfo :: Name -> Type -> IdInfo -> Id
......@@ -311,7 +311,7 @@ mkExportedVanillaId name ty = Var.mkExportedLocalVar VanillaId name ty vanillaId
-- | Create a system local 'Id'. These are local 'Id's (see "Var#globalvslocal")
-- that are created by the compiler out of thin air
mkSysLocal :: FastString -> Unique -> Type -> Id
mkSysLocal fs uniq ty = ASSERT( not (isCoercionType ty) )
mkSysLocal fs uniq ty = ASSERT( not (isCoVarType ty) )
mkLocalId (mkSystemVarName uniq fs) ty
-- | Like 'mkSysLocal', but checks to see if we have a covar type
......@@ -328,7 +328,7 @@ mkSysLocalOrCoVarM fs ty
-- | Create a user local 'Id'. These are local 'Id's (see "Var#globalvslocal") with a name and location that the user might recognize
mkUserLocal :: OccName -> Unique -> Type -> SrcSpan -> Id
mkUserLocal occ uniq ty loc = ASSERT( not (isCoercionType ty) )
mkUserLocal occ uniq ty loc = ASSERT( not (isCoVarType ty) )
mkLocalId (mkInternalName uniq occ loc) ty
-- | Like 'mkUserLocal', but checks if we have a coercion type
......@@ -585,7 +585,7 @@ isDeadBinder bndr | isId bndr = isDeadOcc (idOccInfo bndr)
-}
isEvVar :: Var -> Bool
isEvVar var = isPredTy (varType var)
isEvVar var = isEvVarType (varType var)
isDictId :: Id -> Bool
isDictId id = isDictTy (idType id)
......
......@@ -1214,7 +1214,7 @@ lintCoBndr cv thing_inside
= do { subst <- getTCvSubst
; let (subst', cv') = substCoVarBndr subst cv
; lintKind (varType cv')
; lintL (isCoercionType (varType cv'))
; lintL (isCoVarType (varType cv'))
(text "CoVar with non-coercion type:" <+> pprTyVar cv)
; updateTCvSubst subst' (thing_inside cv') }
......@@ -1260,7 +1260,7 @@ lintIdBndr top_lvl bind_site id linterF
-- Check that the Id does not have type (t1 ~# t2) or (t1 ~R# t2);
-- if so, it should be a CoVar, and checked by lintCoVarBndr
; lintL (not (isCoercionType ty))
; lintL (not (isCoVarType ty))
(text "Non-CoVar has coercion type" <+> ppr id <+> dcolon <+> ppr ty)
; let id' = setIdType id ty
......
......@@ -243,7 +243,7 @@ simple_opt_expr env expr
-- Note [Getting the map/coerce RULE to work]
| isDeadBinder b
, [(DEFAULT, _, rhs)] <- as
, isCoercionType (varType b)
, isCoVarType (varType b)
, (Var fun, _args) <- collectArgs e
, fun `hasKey` coercibleSCSelIdKey
-- without this last check, we get #11230
......
......@@ -266,7 +266,7 @@ mkCast e co
= e
mkCast (Coercion e_co) co
| isCoercionType (pSnd (coercionKind co))
| isCoVarType (pSnd (coercionKind co))
-- The guard here checks that g has a (~#) on both sides,
-- otherwise decomposeCo fails. Can in principle happen
-- with unsafeCoerce
......
......@@ -888,9 +888,9 @@ decomposeRuleLhs dflags orig_bndrs orig_lhs
, text "Orig lhs:" <+> ppr orig_lhs
, text "optimised lhs:" <+> ppr lhs2 ])
pp_bndr bndr
| isTyVar bndr = text "type variable" <+> quotes (ppr bndr)
| Just pred <- evVarPred_maybe bndr = text "constraint" <+> quotes (ppr pred)
| otherwise = text "variable" <+> quotes (ppr bndr)
| isTyVar bndr = text "type variable" <+> quotes (ppr bndr)
| isEvVar bndr = text "constraint" <+> quotes (ppr (varType bndr))
| otherwise = text "variable" <+> quotes (ppr bndr)
constructor_msg con = vcat
[ text "A constructor," <+> ppr con <>
......
......@@ -512,14 +512,14 @@ matchHeteroEquality :: [Type] -> TcM ClsInstResult
-- Solves (t1 ~~ t2)
matchHeteroEquality args
= return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon args ]
, cir_mk_ev = evDFunApp (dataConWrapId heqDataCon) args
, cir_mk_ev = evDataConApp heqDataCon args
, cir_what = BuiltinInstance })
matchHomoEquality :: [Type] -> TcM ClsInstResult
-- Solves (t1 ~ t2)
matchHomoEquality args@[k,t1,t2]
= return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon [k,k,t1,t2] ]
, cir_mk_ev = evDFunApp (dataConWrapId eqDataCon) args
, cir_mk_ev = evDataConApp eqDataCon args
, cir_what = BuiltinInstance })
matchHomoEquality args = pprPanic "matchHomoEquality" (ppr args)
......@@ -527,8 +527,7 @@ matchHomoEquality args = pprPanic "matchHomoEquality" (ppr args)
matchCoercible :: [Type] -> TcM ClsInstResult
matchCoercible args@[k, t1, t2]
= return (OneInst { cir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
, cir_mk_ev = evDFunApp (dataConWrapId coercibleDataCon)
args
, cir_mk_ev = evDataConApp coercibleDataCon args
, cir_what = BuiltinInstance })
where
args' = [k, k, t1, t2]
......
......@@ -23,7 +23,6 @@ import TcEvTerm
import Class
import TyCon
import TyCoRep -- cleverly decomposes types, good for completeness checking
import TysWiredIn( cTupleTyConName )
import Coercion
import CoreSyn
import Id( idType, mkTemplateLocals )
......@@ -488,31 +487,22 @@ mk_strict_superclasses rec_clss ev tvs theta cls tys
size = sizeTypes tys
do_one_given evar given_loc sel_id
| not (null tvs)
, null theta
, isUnliftedType sc_pred
-- Very special case for equality
-- See Note [Equality superclasses in quantified constraints]
= do { empty_ctuple_cls <- tcLookupClass (cTupleTyConName 0)
; let theta1 = [mkClassPred empty_ctuple_cls []]
dict_ids1 = mkTemplateLocals theta1
; given_ev <- new_given theta1 dict_ids1 []
; return [mkNonCanonical given_ev] }
| otherwise -- Normal case
= do { given_ev <- new_given theta dict_ids dict_ids
| isUnliftedType sc_pred
, not (null tvs && null theta)
= -- See Note [Equality superclasses in quantified constraints]
return []
| otherwise
= do { given_ev <- newGivenEvVar given_loc $
(given_ty, mk_sc_sel evar sel_id)
; mk_superclasses rec_clss given_ev tvs theta sc_pred }
where
sc_pred = funResultTy (piResultTys (idType sel_id) tys)
sc_pred = funResultTy (piResultTys (idType sel_id) tys)
given_ty = mkInfSigmaTy tvs theta sc_pred
new_given theta_abs dict_ids_abs dict_ids_app
= newGivenEvVar given_loc (given_ty, given_ev)
where
given_ty = mkInfSigmaTy tvs theta_abs sc_pred
given_ev = EvExpr $ mkLams tvs $ mkLams dict_ids_abs $
Var sel_id `mkTyApps` tys `App`
(evId evar `mkTyApps` mkTyVarTys tvs `mkVarApps` dict_ids_app)
mk_sc_sel evar sel_id
= EvExpr $ mkLams tvs $ mkLams dict_ids $
Var sel_id `mkTyApps` tys `App`
(evId evar `mkTyApps` mkTyVarTys tvs `mkVarApps` dict_ids)
mk_given_loc loc
| isCTupleClass cls
......@@ -609,24 +599,22 @@ There is a wrinkle though, in the case where 'theta' is empty, so
we have
f :: (forall a. a~b) => stuff
Now the superclass machinery kicks in, in makeSuperClasses,
giving us a a second quantified constrait
Now, potentially, the superclass machinery kicks in, in
makeSuperClasses, giving us a a second quantified constrait
(forall a. a ~# b)
BUT this is an unboxed value! And nothing has prepared us for
dictionary "functions" that are unboxed. Actually it does just
about work, but the simplier ends up with stuff like
case (/\a. eq_sel d) of df -> ...(df @Int)...
and fails to simplify that any further.
and fails to simplify that any further. And it doesn't satisfy
isPredTy any more.
It seems eaiser to give such unboxed quantifed constraints a
dummmy () argument, thus
(forall a. (% %) => a ~# b)
where (% %) is the empty constraint tuple. That makes everything
be nicely boxed.
So for now we simply decline to take superclasses in the quantified
case. Instead we have a special case in TcInteract.doTopReactOther,
which looks for primitive equalities specially in the quantified
constraints.
(One might wonder about using void# instead, but this seems more
uniform -- it's a constraint argument -- and I'm not worried about
the last drop of efficiency for this very rare case.)
See also Note [Evidence for quantified constraints] in Type.
************************************************************************
......
......@@ -1186,8 +1186,8 @@ mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_hole = hole })
pp_hole_type_with_kind
| isLiftedTypeKind hole_kind
|| isCoercionType hole_ty -- Don't print the kind of unlifted
-- equalities (#15039)
|| isCoVarType hole_ty -- Don't print the kind of unlifted
-- equalities (#15039)
= pprType hole_ty
| otherwise
= pprType hole_ty <+> dcolon <+> pprKind hole_kind
......
......@@ -20,7 +20,7 @@ module TcEvidence (
-- EvTerm (already a CoreExpr)
EvTerm(..), EvExpr,
evId, evCoercion, evCast, evDFunApp, evSelector,
evId, evCoercion, evCast, evDFunApp, evDataConApp, evSelector,
mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars,
evTermCoercion, evTermCoercion_maybe,
......@@ -56,6 +56,7 @@ import PprCore () -- Instance OutputableBndr TyVar
import TcType
import Type
import TyCon
import DataCon( DataCon, dataConWrapId )
import Class( Class )
import PrelNames
import DynFlags ( gopt, GeneralFlag(Opt_PrintTypecheckerElaboration) )
......@@ -552,6 +553,9 @@ evCast et tc | isReflCo tc = EvExpr et
evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm
evDFunApp df tys ets = EvExpr $ Var df `mkTyApps` tys `mkApps` ets
evDataConApp :: DataCon -> [Type] -> [EvExpr] -> EvTerm
evDataConApp dc tys ets = evDFunApp (dataConWrapId dc) tys ets
-- Selector id plus the types at which it
-- should be instantiated, used for HasField
-- dictionaries; see Note [HasField instances]
......
......@@ -39,6 +39,7 @@ import TcSMonad
import Bag
import MonadUtils ( concatMapM, foldlM )
import CoreSyn
import Data.List( partition, foldl', deleteFirstsBy )
import SrcLoc
import VarEnv
......@@ -1827,14 +1828,51 @@ doTopReactOther :: Ct -> TcS (StopOrContinue Ct)
-- Why equalities? See TcCanonical
-- Note [Equality superclasses in quantified constraints]
doTopReactOther work_item
= do { res <- matchLocalInst pred (ctEvLoc ev)
| isGiven ev
= continueWith work_item
| EqPred eq_rel t1 t2 <- classifyPredType pred
= -- See Note [Looking up primitive equalities in quantified constraints]
case boxEqPred eq_rel t1 t2 of
Nothing -> continueWith work_item
Just (cls, tys)
-> do { res <- matchLocalInst (mkClassPred cls tys) loc
; case res of
OneInst { cir_mk_ev = mk_ev }
-> chooseInstance work_item
(res { cir_mk_ev = mk_eq_ev cls tys mk_ev })
where
_ -> continueWith work_item }
| otherwise
= do { res <- matchLocalInst pred loc
; case res of
OneInst {} -> chooseInstance work_item res
_ -> continueWith work_item }
where
ev = ctEvidence work_item
loc = ctEvLoc ev
pred = ctEvPred ev
mk_eq_ev cls tys mk_ev evs
= case (mk_ev evs) of
EvExpr e -> EvExpr (Var sc_id `mkTyApps` tys `App` e)
ev -> pprPanic "mk_eq_ev" (ppr ev)
where
[sc_id] = classSCSelIds cls
{- Note [Looking up primitive equalities in quantified constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For equalities (a ~# b) look up (a ~ b), and then do a superclass
selection. This avoids having to support quantified constraints whose
kind is not Constraint, such as (forall a. F a ~# b)
See
* Note [Evidence for quantified constraints] in Type
* Note [Equality superclasses in quantified constraints]
in TcCanonical
-}
--------------------
doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
......@@ -2539,8 +2577,8 @@ nullary case of what's happening here.
-}
matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
-- Try any Given quantified constraints, which are
-- effectively just local instance declarations.
-- Look up the predicate in Given quantified constraints,
-- which are effectively just local instance declarations.
matchLocalInst pred loc
= do { ics <- getInertCans
; case match_local_inst (inert_insts ics) of
......
......@@ -41,6 +41,8 @@ import TcBinds
import BasicTypes
import TcSimplify
import TcUnify
import Type( PredTree(..), EqRel(..), classifyPredType )
import TysWiredIn
import TcType
import TcEvidence
import BuildTyCl
......@@ -52,6 +54,7 @@ import FieldLabel
import Bag
import Util
import ErrUtils
import Data.Maybe( mapMaybe )
import Control.Monad ( zipWithM )
import Data.List( partition )
......@@ -157,8 +160,9 @@ tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
; prov_dicts <- mapM zonkId prov_dicts
; let filtered_prov_dicts = mkMinimalBySCs evVarPred prov_dicts
prov_theta = map evVarPred filtered_prov_dicts
-- Filtering: see Note [Remove redundant provided dicts]
(prov_theta, prov_evs)
= unzip (mapMaybe mkProvEvidence filtered_prov_dicts)
-- Report bad universal type variables
-- See Note [Type variables whose kind is captured]
......@@ -181,12 +185,38 @@ tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
(mkTyVarBinders Inferred univ_tvs
, req_theta, ev_binds, req_dicts)
(mkTyVarBinders Inferred ex_tvs
, mkTyVarTys ex_tvs, prov_theta
, map (EvExpr . evId) filtered_prov_dicts)
, mkTyVarTys ex_tvs, prov_theta, prov_evs)
(map nlHsVar args, map idType args)
pat_ty rec_fields } }
tcInferPatSynDecl (XPatSynBind _) = panic "tcInferPatSynDecl"
mkProvEvidence :: EvId -> Maybe (PredType, EvTerm)
-- See Note [Equality evidence in pattern synonyms]
mkProvEvidence ev_id
| EqPred r ty1 ty2 <- classifyPredType pred
, let k1 = typeKind ty1
k2 = typeKind ty2
is_homo = k1 `tcEqType` k2
homo_tys = [k1, ty1, ty2]
hetero_tys = [k1, k2, ty1, ty2]
= case r of
ReprEq | is_homo
-> Just ( mkClassPred coercibleClass homo_tys
, evDataConApp coercibleDataCon homo_tys eq_con_args )
| otherwise -> Nothing
NomEq | is_homo
-> Just ( mkClassPred eqClass homo_tys
, evDataConApp eqDataCon homo_tys eq_con_args )
| otherwise
-> Just ( mkClassPred heqClass hetero_tys
, evDataConApp heqDataCon hetero_tys eq_con_args )
| otherwise
= Just (pred, EvExpr (evId ev_id))
where
pred = evVarPred ev_id
eq_con_args = [evId ev_id]
badUnivTvErr :: [TyVar] -> TyVar -> TcM ()
-- See Note [Type variables whose kind is captured]
badUnivTvErr ex_tvs bad_tv
......@@ -239,6 +269,30 @@ Similarly consider
The pattern (Bam x y) binds two (Ord a) dictionaries, but we only
need one. Agian mkMimimalWithSCs removes the redundant one.
Note [Equality evidence in pattern synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
data X a where
MkX :: Eq a => [a] -> X (Maybe a)
pattern P x = MkG x
Then there is a danger that GHC will infer
P :: forall a. () =>
forall b. (a ~# Maybe b, Eq b) => [b] -> X a
The 'builder' for P, which is called in user-code, will then
have type
$bP :: forall a b. (a ~# Maybe b, Eq b) => [b] -> X a
and that is bad because (a ~# Maybe b) is not a predicate type
(see Note [Types for coercions, predicates, and evidence] in Type)
and is not implicitly instantiated.
So in mkProvEvidence we lift (a ~# b) to (a ~ b). Tiresome, and
marginally less efficient, if the builder/martcher are not inlined.
See also Note [Lift equality constaints when quantifying] in TcType
Note [Type variables whose kind is captured]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
......
......@@ -90,14 +90,13 @@ module TcType (
deNoteType,
orphNamesOfType, orphNamesOfCo,
orphNamesOfTypes, orphNamesOfCoCon,
getDFunTyKey,
evVarPred_maybe, evVarPred,
getDFunTyKey, evVarPred,
---------------------------------
-- Predicate types
mkMinimalBySCs, transSuperClasses,
pickQuantifiablePreds, pickCapturedPreds,
immSuperClasses,
immSuperClasses, boxEqPred,
isImprovementPred,
-- * Finding type instances
......@@ -215,7 +214,7 @@ import Name -- hiding (varName)
import NameSet
import VarEnv
import PrelNames
import TysWiredIn( coercibleClass, unitTyCon, unitTyConKey
import TysWiredIn( coercibleClass, eqClass, heqClass, unitTyCon, unitTyConKey
, listTyCon, constraintKind )
import BasicTypes
import Util
......@@ -1986,18 +1985,12 @@ hasTyVarHead ty -- Haskell 98 allows predicates of form
Just (ty, _) -> hasTyVarHead ty
Nothing -> False
evVarPred_maybe :: EvVar -> Maybe PredType
evVarPred_maybe v = if isPredTy ty then Just ty else Nothing
where ty = varType v
evVarPred :: EvVar -> PredType
evVarPred var
| debugIsOn
= case evVarPred_maybe var of
Just pred -> pred
Nothing -> pprPanic "tcEvVarPred" (ppr var <+> ppr (varType var))
| otherwise
= varType var
= ASSERT2( isEvVarType var_ty, ppr var <+> dcolon <+> ppr var_ty )
var_ty
where
var_ty = varType var
------------------
-- | When inferring types, should we quantify over a given predicate?
......@@ -2015,31 +2008,38 @@ pickQuantifiablePreds qtvs theta
= let flex_ctxt = True in -- Quantify over non-tyvar constraints, even without
-- -XFlexibleContexts: see Trac #10608, #10351
-- flex_ctxt <- xoptM Opt_FlexibleContexts
filter (pick_me flex_ctxt) theta
mapMaybe (pick_me flex_ctxt) theta
where
pick_me flex_ctxt pred
= case classifyPredType pred of
ClassPred cls tys
| Just {} <- isCallStackPred cls tys
-- NEVER infer a CallStack constraint
-- Otherwise, we let the constraints bubble up to be
-- solved from the outer context, or be defaulted when we
-- reach the top-level.
-- see Note [Overview of implicit CallStacks]
-> False
-- NEVER infer a CallStack constraint. Otherwise we let
-- the constraints bubble up to be solved from the outer
-- context, or be defaulted when we reach the top-level.
-- See Note [Overview of implicit CallStacks]
-> Nothing
| isIPClass cls -> True -- See note [Inheriting implicit parameters]
| isIPClass cls
-> Just pred -- See note [Inheriting implicit parameters]
| otherwise
-> pick_cls_pred flex_ctxt cls tys
| pick_cls_pred flex_ctxt cls tys
-> Just pred
EqPred ReprEq ty1 ty2 -> pick_cls_pred flex_ctxt coercibleClass [ty1, ty2]
-- representational equality is like a class constraint
EqPred eq_rel ty1 ty2
| quantify_equality eq_rel ty1 ty2
, Just (cls, tys) <- boxEqPred eq_rel ty1 ty2
-- boxEqPred: See Note [Lift equality constaints when quantifying]
, pick_cls_pred flex_ctxt cls tys
-> Just (mkClassPred cls tys)
IrredPred ty
| tyCoVarsOfType ty `intersectsVarSet` qtvs
-> Just pred
_ -> Nothing
EqPred NomEq ty1 ty2 -> quant_fun ty1 || quant_fun ty2
IrredPred ty -> tyCoVarsOfType ty `intersectsVarSet` qtvs
ForAllPred {} -> False
pick_cls_pred flex_ctxt cls tys
= tyCoVarsOfTypes tys `intersectsVarSet` qtvs
......@@ -2048,12 +2048,31 @@ pickQuantifiablePreds qtvs theta
-- will pass! See Trac #10351.
-- See Note [Quantifying over equality constraints]
quantify_equality NomEq ty1 ty2 = quant_fun ty1 || quant_fun ty2
quantify_equality ReprEq _ _ = True
quant_fun ty
= case tcSplitTyConApp_maybe ty of
Just (tc, tys) | isTypeFamilyTyCon tc
-> tyCoVarsOfTypes tys `intersectsVarSet` qtvs
_ -> False
boxEqPred :: EqRel -> Type -> Type -> Maybe (Class, [Type])
-- Given (t1 ~# t2) or (t1 ~R# t2) return the boxed version
-- (t1 ~ t2) or (t1 `Coercible` t2)
boxEqPred eq_rel ty1 ty2
= case eq_rel of
NomEq | homo_kind -> Just (eqClass, [k1, ty1, ty2])
| otherwise -> Just (heqClass, [k1, k2, ty1, ty2])
ReprEq | homo_kind -> Just (coercibleClass, [k1, ty1, ty2])
| otherwise -> Nothing -- Sigh: we do not have hererogeneous Coercible
-- so we can't abstract over it
-- Nothing fundamental: we could add it
where
k1 = typeKind ty1
k2 = typeKind ty2
homo_kind = k1 `tcEqType` k2
pickCapturedPreds
:: TyVarSet -- Quantifying over these
-> TcThetaType -- Proposed constraints to quantify
......@@ -2210,6 +2229,18 @@ Notice that
See also TcTyDecls.checkClassCycles.
Note [Lift equality constaints when quantifying]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We can't quantify over a constraint (t1 ~# t2) because that isn't a
predicate type; see Note [Types for coercions, predicates, and evidence]
in Type.hs.
So we have to 'lift' it to (t1 ~ t2). Similarly (~R#) must be lifted
to Coercible.
This tiresome lifting is the reason that pick_me (in
pickQuantifiablePreds) returns a Maybe rather than a Bool.
Note [Quantifying over equality constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Should we quantify over an equality constraint (s ~ t)? In general, we don't.
......
......@@ -46,7 +46,7 @@ module TyCoRep (
mkPiTys,
isTYPE,
isLiftedTypeKind, isUnliftedTypeKind,
isCoercionType, isRuntimeRepTy, isRuntimeRepVar,
isRuntimeRepTy, isRuntimeRepVar,
sameVis,
-- * Functions over binders
......@@ -841,17 +841,6 @@ mkTyCoPiTys tbs ty = foldr mkTyCoPiTy ty tbs
mkPiTys :: [TyCoBinder] -> Type -> Type
mkPiTys tbs ty = foldr mkPiTy ty tbs
-- | Does this type classify a core (unlifted) Coercion?
-- At either role nominal or representational
-- (t1 ~# t2) or (t1 ~R# t2)
isCoercionType :: Type -> Bool
isCoercionType (TyConApp tc tys)
| (tc `hasKey` eqPrimTyConKey) || (tc `hasKey` eqReprPrimTyConKey)
, tys `lengthIs` 4
= True
isCoercionType _ = False
-- | Create the plain type constructor type which has been applied to no type arguments at all.
mkTyConTy :: TyCon -> Type
mkTyConTy tycon = TyConApp tycon []
......
......@@ -110,9 +110,10 @@ module Type (
-- ** Predicates on types
isTyVarTy, isFunTy, isDictTy, isPredTy, isCoercionTy,
isCoercionTy_maybe, isCoercionType, isForAllTy,
isCoercionTy_maybe, isForAllTy,
isForAllTy_ty, isForAllTy_co,
isPiTy, isTauTy, isFamFreeTy,
isCoVarType, isEvVarType,
isValidJoinPointType,
......@@ -1694,6 +1695,36 @@ caseBinder (Anon t) _ d = d t
Predicates on PredType
Note [Types for coercions, predicates, and evidence]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We treat differently:
(a) Predicate types
Test: isPredTy
Binders: DictIds
Kind: Constraint
Examples: (Eq a), and (a ~ b)
(b) Coercion types are primitive, unboxed equalities
Test: isCoVarTy
Binders: CoVars (can appear in coercions)
Kind: TYPE (TupleRep [])
Examples: (t1 ~# t2) or (t1 ~R# t2)
(c) Evidence types is the type of evidence manipulated by
the type constraint solver.
Test: isEvVarType
Binders: EvVars
Kind: Constraint or TYPE (TupleRep [])
Examples: all coercion types and predicate types
Coercion types and predicate types are mutually exclusive,
but evidence types are a superset of both.
When treated as a user type, predicates are invisible and are
implicitly instantiated; but coercion types, and non-pred evidence
types, are just regular old types.
Note [isPredTy complications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
You would think that we could define
......@@ -1714,6 +1745,19 @@ But there are a number of complications:
print it as such. But that means that isPredTy must return True for
(C a => C [a]). Admittedly that type is illegal in Haskell, but we
want to print it nicely in error messages.
Note [Evidence for quantified constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The superclass mechanism in TcCanonical.makeSuperClasses risks
taking a quantified constraint like
(forall a. C a => a ~ b)
and generate superclass evidence
(forall a. C a => a ~# b)
This is a funny thing: neither isPredTy nor isCoVarType are true
of it. So we are careful not to generate it in the first place:
see Note [Equality superclasses in quantified constraints]
in TcCanonical.
-}
-- | Split a type constructor application into its type constructor and
......@@ -1766,16 +1810,39 @@ tcReturnsConstraintKind (FunTy _ ty) = tcReturnsConstraintKind ty
tcReturnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc
tcReturnsConstraintKind _ = False
isEvVarType :: Type -> Bool
-- True of (a) predicates, of kind Constraint, such as (Eq a), and (a ~ b)
-- (b) coercion types, such as (t1 ~# t2) or (t1 ~R# t2)
-- See Note [Types for coercions, predicates, and evidence]
-- See Note [Evidence for quantified constraints]
isEvVarType ty = isCoVarType ty || isPredTy ty
-- | Does this type classify a core (unlifted) Coercion?
-- At either role nominal or representational
-- (t1 ~# t2) or (t1 ~R# t2)
-- See Note [Types for coercions, predicates, and evidence]
isCoVarType :: Type -> Bool
isCoVarType ty
| Just (tc,tys) <- splitTyConApp_maybe ty
, (tc `hasKey` eqPrimTyConKey) || (tc `hasKey` eqReprPrimTyConKey)
, tys `lengthIs` 4
= True
isCoVarType _ = False
-- | Is the type suitable to classify a given/wanted in the typechecker?
isPredTy :: Type -> Bool
-- See Note [isPredTy complications]
-- NB: /not/ true of (t1 ~# t2) or (t1 ~R# t2)
-- See Note [Types for coercions, predicates, and evidence]
isPredTy ty = go ty []