[commit: ghc] wip/rae-new-coercible: Check validity of EqPred ReprEq correctly (ada2776)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/rae-new-coercible
Link       : http://ghc.haskell.org/trac/ghc/changeset/ada2776b77d042866035d5800d1727cc872fccd6/ghc

>---------------------------------------------------------------

commit ada2776b77d042866035d5800d1727cc872fccd6
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date:   Fri Nov 28 17:09:49 2014 -0500

    Check validity of EqPred ReprEq correctly


>---------------------------------------------------------------

ada2776b77d042866035d5800d1727cc872fccd6
 compiler/typecheck/TcValidity.lhs | 42 +++++++++++++++++++++++----------------
 1 file changed, 25 insertions(+), 17 deletions(-)

diff --git a/compiler/typecheck/TcValidity.lhs b/compiler/typecheck/TcValidity.lhs
index d8e2721..d62fe38 100644
--- a/compiler/typecheck/TcValidity.lhs
+++ b/compiler/typecheck/TcValidity.lhs
@@ -502,7 +502,7 @@ check_pred_help under_syn dflags ctxt pred
   = case classifyPredType pred of
       ClassPred cls tys     -> check_class_pred dflags ctxt pred cls tys
       EqPred NomEq _ _      -> check_eq_pred    dflags pred
-      EqPred ReprEq ty1 ty2 -> check_class_pred dflags ctxt pred coercibleClass [ty1, ty2]
+      EqPred ReprEq ty1 ty2 -> check_repr_eq_pred dflags ctxt pred ty1 ty2
       TuplePred tys         -> check_tuple_pred under_syn dflags ctxt pred tys
       IrredPred _           -> check_irred_pred under_syn dflags ctxt pred
 
@@ -515,27 +515,31 @@ check_class_pred dflags ctxt pred cls tys
                  (badIPPred pred)
 
                 -- Check the form of the argument types
-       ; checkTc (check_class_pred_tys dflags ctxt tys)
-                 (predTyVarErr (mkClassPred cls tys) $$ how_to_allow)
+       ; check_class_pred_tys dflags ctxt pred tys
        }
   where
     class_name = className cls
     arity      = classArity cls
     n_tys      = length tys
     arity_err  = arityErr "Class" class_name arity n_tys
-    how_to_allow = parens (ptext (sLit "Use FlexibleContexts to permit this"))
 
 check_eq_pred :: DynFlags -> PredType -> TcM ()
 check_eq_pred dflags pred
-  =       -- Equational constraints are valid in all contexts if type
-          -- families are permitted
+  =         -- Equational constraints are valid in all contexts if type
+            -- families are permitted
     checkTc (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags) 
             (eqPredTyErr pred)
 
-check_tuple_pred :: Bool -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
-check_tuple_pred under_syn dflags ctxt pred ts
-  = do {   -- See Note [ConstraintKinds in predicates]
-         checkTc (under_syn || xopt Opt_ConstraintKinds dflags)
+check_repr_eq_pred :: DynFlags -> UserTypeCtxt -> PredType -> TcType -> TcType -> TcM ()
+check_repr_eq_pred dflags ctxt pred ty1 ty2
+  = do { mapM_ checkValidMonoType tys
+       ; check_class_pred_tys dflags ctxt pred tys }
+  where
+    tys = [ty1, ty2]
+
+check_tuple_pred :: DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
+check_tuple_pred dflags ctxt pred ts
+  = do { checkTc (xopt Opt_ConstraintKinds dflags)
                  (predTupleErr pred)
        ; mapM_ (check_pred_help under_syn dflags ctxt) ts }
     -- This case will not normally be executed because without
@@ -587,18 +591,22 @@ It is equally dangerous to allow them in instance heads because in that case the
 Paterson conditions may not detect duplication of a type variable or size change. -}
 
 -------------------------
-check_class_pred_tys :: DynFlags -> UserTypeCtxt -> [KindOrType] -> Bool
-check_class_pred_tys dflags ctxt kts
-  = case ctxt of
+check_class_pred_tys :: DynFlags -> UserTypeCtxt -> PredType -> [KindOrType] -> TcM ()
+check_class_pred_tys dflags ctxt pred kts
+  = checkTc pred_ok (predTyVarErr pred $$ how_to_allow)
+  where
+    (_, tys) = span isKind kts  -- see Note [Kind polymorphic type classes]
+    flexible_contexts = xopt Opt_FlexibleContexts dflags
+    undecidable_ok = xopt Opt_UndecidableInstances dflags
+
+    pred_ok = case ctxt of
         SpecInstCtxt -> True    -- {-# SPECIALISE instance Eq (T Int) #-} is fine
         InstDeclCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
                                 -- Further checks on head and theta in
                                 -- checkInstTermination
         _             -> flexible_contexts || all tyvar_head tys
-  where
-    (_, tys) = span isKind kts  -- see Note [Kind polymorphic type classes]
-    flexible_contexts = xopt Opt_FlexibleContexts dflags
-    undecidable_ok = xopt Opt_UndecidableInstances dflags
+    how_to_allow = parens (ptext (sLit "Use FlexibleContexts to permit this"))
+
 
 -------------------------
 tyvar_head :: Type -> Bool