From 0faf7fd3e6c652575af9993787f07cad86f452f6 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Tue, 16 Oct 2018 12:38:16 +0100 Subject: 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. --- compiler/deSugar/DsBinds.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'compiler/deSugar') diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs index 421adcaccd..f2ff5dd623 100644 --- a/compiler/deSugar/DsBinds.hs +++ b/compiler/deSugar/DsBinds.hs @@ -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 <> -- cgit v1.2.1