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.

1 files changed, 57 insertions, 3 deletions

diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index a2406df319..8f59e39a4f 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -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