diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-10-16 12:38:16 +0100 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2018-10-24 16:38:55 +0100 |
commit | 0faf7fd3e6c652575af9993787f07cad86f452f6 (patch) | |
tree | 029d5a626ac2677305151120cd4a0a4a144c6493 /compiler/typecheck/TcInteract.hs | |
parent | 321bc1a644a9e4598a4af30d4aeae315f0ff487a (diff) | |
download | haskell-0faf7fd3e6c652575af9993787f07cad86f452f6.tar.gz |
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.
Diffstat (limited to 'compiler/typecheck/TcInteract.hs')
-rw-r--r-- | compiler/typecheck/TcInteract.hs | 44 |
1 files changed, 41 insertions, 3 deletions
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 1771e19849..3914db6c13 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -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 |