From 0faf7fd3e6c652575af9993787f07cad86f452f6 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
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/typecheck/TcInteract.hs | 44 +++++++++++++++++++++++++++++++++++++---
 1 file changed, 41 insertions(+), 3 deletions(-)

(limited to 'compiler/typecheck/TcInteract.hs')

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
-- 
cgit v1.2.1