Allow (~) in the head of a quantified constraints

Since the introduction of quantified constraints, GHC has rejected
a quantified constraint with (~) in the head, thus
  f :: (forall a. blah => a ~ ty) => stuff

I am frankly dubious that this is ever useful.  But /is/ necessary for
Coercible (representation equality version of (~)) and it does no harm
to allow it for (~) as well.  Plus, our users are asking for it
(Trac #15359, #15625).

It was really only excluded by accident, so
this patch lifts the restriction. See TcCanonical
Note [Equality superclasses in quantified constraints]

There are a number of wrinkles:

* If the context of the quantified constraint is empty, we
  can get trouble when we get down to unboxed equality (a ~# b)
  or (a ~R# b), as Trac #15625 showed. This is even more of
  a corner case, but it produced an outright crash, so I elaborated
  the superclass machinery in TcCanonical.makeStrictSuperClasses
  to add a void argument in this case.  See
  Note [Equality superclasses in quantified constraints]

* The restriction on (~) was in TcValidity.checkValidInstHead.
  In lifting the restriction I discovered an old special case for
  (~), namely
      | clas_nm `elem` [ heqTyConName, eqTyConName]
      , nameModule clas_nm /= this_mod
  This was (solely) to support the strange instance
      instance a ~~ b => a ~ b
  in Data.Type.Equality. But happily that is no longer
  with us, since
     commit f265008fb6f70830e7e92ce563f6d83833cef071
     Refactor (~) to reduce the suerpclass stack
  So I removed the special case.

* I found that the Core invariants on when we could have
       co = <expr>
  were entirely not written down. (Getting this wrong ws
  the proximate source of the crash in Trac #15625.  So

  - Documented them better in CoreSyn
      Note [CoreSyn type and coercion invariant],
  - Modified CoreOpt and CoreLint to match
  - Modified CoreUtils.bindNonRec to match
  - Made MkCore.mkCoreLet use bindNonRec, rather
    than duplicate its logic
  - Made Simplify.rebuildCase case-to-let respect
      Note [CoreSyn type and coercion invariant],

14 files changed, 249 insertions, 73 deletions

diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 6dee383cd9..349d36d8e2 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -519,6 +519,11 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
        ; binder_ty <- applySubstTy (idType binder)
        ; ensureEqTys binder_ty ty (mkRhsMsg binder (text "RHS") ty)
 
+       -- If the binding is for a CoVar, the RHS should be (Coercion co)
+       -- See Note [CoreSyn type and coercion invariant] in CoreSyn
+       ; checkL (not (isCoVar binder) || isCoArg rhs)
+                (mkLetErr binder rhs)
+
        -- Check that it's not levity-polymorphic
        -- Do this first, because otherwise isUnliftedType panics
        -- Annoyingly, this duplicates the test in lintIdBdr,
@@ -842,6 +847,7 @@ lintVarOcc :: Var -> Int -- Number of arguments (type or value) being passed
 lintVarOcc var nargs
   = do  { checkL (isNonCoVarId var)
                  (text "Non term variable" <+> ppr var)
+                 -- See CoreSyn Note [Variable occurrences in Core]
 
         -- Cneck that the type of the occurrence is the same
         -- as the type of the binding site
diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs
index 8a41c98822..3254d7334c 100644
--- a/compiler/coreSyn/CoreOpt.hs
+++ b/compiler/coreSyn/CoreOpt.hs
@@ -32,7 +32,7 @@ import PprCore  ( pprCoreBindings, pprRules )
 import OccurAnal( occurAnalyseExpr, occurAnalysePgm )
 import Literal  ( Literal(MachStr) )
 import Id
-import Var      ( varType )
+import Var      ( varType, isNonCoVarId )
 import VarSet
 import VarEnv
 import DataCon
@@ -360,7 +360,10 @@ simple_bind_pair env@(SOE { soe_inl = inl_env, soe_subst = subst })
   = ASSERT( isCoVar in_bndr )
     (env { soe_subst = extendCvSubst subst in_bndr out_co }, Nothing)
 
-  | pre_inline_unconditionally
+  | ASSERT2( isNonCoVarId in_bndr, ppr in_bndr )
+    -- The previous two guards got rid of tyvars and coercions
+    -- See Note [CoreSyn type and coercion invariant] in CoreSyn
+    pre_inline_unconditionally
   = (env { soe_inl = extendVarEnv inl_env in_bndr clo }, Nothing)
 
   | otherwise
@@ -385,12 +388,11 @@ simple_bind_pair env@(SOE { soe_inl = inl_env, soe_subst = subst })
 
     pre_inline_unconditionally :: Bool
     pre_inline_unconditionally
-       | isCoVar in_bndr          = False    -- See Note [Do not inline CoVars unconditionally]
-       | isExportedId in_bndr     = False    --     in SimplUtils
+       | isExportedId in_bndr     = False
        | stable_unf               = False
        | not active               = False    -- Note [Inline prag in simplOpt]
        | not (safe_to_inline occ) = False
-       | otherwise = True
+       | otherwise                = True
 
         -- Unconditionally safe to inline
     safe_to_inline :: OccInfo -> Bool
@@ -423,7 +425,10 @@ simple_out_bind_pair :: SimpleOptEnv
                      -> (SimpleOptEnv, Maybe (OutVar, OutExpr))
 simple_out_bind_pair env in_bndr mb_out_bndr out_rhs
                      occ_info active stable_unf
-  | post_inline_unconditionally
+  | ASSERT2( isNonCoVarId in_bndr, ppr in_bndr )
+    -- Type and coercion bindings are caught earlier
+    -- See Note [CoreSyn type and coercion invariant]
+    post_inline_unconditionally
   = ( env' { soe_subst = extendIdSubst (soe_subst env) in_bndr out_rhs }
     , Nothing)
 
@@ -437,14 +442,16 @@ simple_out_bind_pair env in_bndr mb_out_bndr out_rhs
 
     post_inline_unconditionally :: Bool
     post_inline_unconditionally
-       | not active                  = False
-       | isWeakLoopBreaker occ_info  = False -- If it's a loop-breaker of any kind, don't inline
-                                             -- because it might be referred to "earlier"
-       | stable_unf                  = False -- Note [Stable unfoldings and postInlineUnconditionally]
-       | isExportedId in_bndr        = False -- Note [Exported Ids and trivial RHSs]
-       | exprIsTrivial out_rhs       = True
-       | coercible_hack              = True
-       | otherwise                   = False
+       | isExportedId in_bndr  = False -- Note [Exported Ids and trivial RHSs]
+       | stable_unf            = False -- Note [Stable unfoldings and postInlineUnconditionally]
+       | not active            = False --     in SimplUtils
+       | is_loop_breaker       = False -- If it's a loop-breaker of any kind, don't inline
+                                       -- because it might be referred to "earlier"
+       | exprIsTrivial out_rhs = True
+       | coercible_hack        = True
+       | otherwise             = False
+
+    is_loop_breaker = isWeakLoopBreaker occ_info
 
     -- See Note [Getting the map/coerce RULE to work]
     coercible_hack | (Var fun, args) <- collectArgs out_rhs
diff --git a/compiler/coreSyn/CoreSyn.hs b/compiler/coreSyn/CoreSyn.hs
index 025c19e3ca..aa27d7a7fb 100644
--- a/compiler/coreSyn/CoreSyn.hs
+++ b/compiler/coreSyn/CoreSyn.hs
@@ -46,7 +46,7 @@ module CoreSyn (
         exprToType, exprToCoercion_maybe,
         applyTypeToArg,
 
-        isValArg, isTypeArg, isTyCoArg, valArgCount, valBndrCount,
+        isValArg, isTypeArg, isCoArg, isTyCoArg, valArgCount, valBndrCount,
         isRuntimeArg, isRuntimeVar,
 
         -- * Tick-related functions
@@ -173,6 +173,7 @@ These data types are the heart of the compiler
 -- The language consists of the following elements:
 --
 -- *  Variables
+--    See Note [Variable occurrences in Core]
 --
 -- *  Primitive literals
 --
@@ -187,29 +188,10 @@ These data types are the heart of the compiler
 --    this corresponds to allocating a thunk for the things
 --    bound and then executing the sub-expression.
 --
---    #top_level_invariant#
---    #letrec_invariant#
---
---    The right hand sides of all top-level and recursive @let@s
---    /must/ be of lifted type (see "Type#type_classification" for
---    the meaning of /lifted/ vs. /unlifted/). There is one exception
---    to this rule, top-level @let@s are allowed to bind primitive
---    string literals, see Note [CoreSyn top-level string literals].
---
+--    See Note [CoreSyn letrec invariant]
 --    See Note [CoreSyn let/app invariant]
 --    See Note [Levity polymorphism invariants]
---
---    #type_let#
---    We allow a /non-recursive/ let to bind a type variable, thus:
---
---    > Let (NonRec tv (Type ty)) body
---
---    This can be very convenient for postponing type substitutions until
---    the next run of the simplifier.
---
---    At the moment, the rest of the compiler only deals with type-let
---    in a Let expression, rather than at top level.  We may want to revist
---    this choice.
+--    See Note [CoreSyn type and coercion invariant]
 --
 -- *  Case expression. Operationally this corresponds to evaluating
 --    the scrutinee (expression examined) to weak head normal form
@@ -371,13 +353,25 @@ PrelRules for the rationale for this restriction.
 
 -------------------------- CoreSyn INVARIANTS ---------------------------
 
-Note [CoreSyn top-level invariant]
+Note [Variable occurrences in Core]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-See #toplevel_invariant#
+Variable /occurrences/ are never CoVars, though /bindings/ can be.
+All CoVars appear in Coercions.
+
+For example
+  \(c :: Age~#Int) (d::Int). d |> (sym c)
+Here 'c' is a CoVar, which is lambda-bound, but it /occurs/ in
+a Coercion, (sym c).
 
 Note [CoreSyn letrec invariant]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-See #letrec_invariant#
+The right hand sides of all top-level and recursive @let@s
+/must/ be of lifted type (see "Type#type_classification" for
+the meaning of /lifted/ vs. /unlifted/).
+
+There is one exception to this rule, top-level @let@s are
+allowed to bind primitive string literals: see
+Note [CoreSyn top-level string literals].
 
 Note [CoreSyn top-level string literals]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -451,6 +445,27 @@ which will generate a @case@ if necessary
 The let/app invariant is initially enforced by mkCoreLet and mkCoreApp in
 coreSyn/MkCore.
 
+Note [CoreSyn type and coercion invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We allow a /non-recursive/, /non-top-level/ let to bind type and
+coercion variables.  These can be very convenient for postponing type
+substitutions until the next run of the simplifier.
+
+* A type variable binding must have a RHS of (Type ty)
+
+* A coercion variable binding must have a RHS of (Coercion co)
+
+  It is possible to have terms that return a coercion, but we use
+  case-binding for those; e.g.
+     case (eq_sel d) of (co :: a ~# b) -> blah
+  where eq_sel :: (a~b) -> (a~#b)
+
+  Or even even
+      case (df @Int) of (co :: a ~# b) -> blah
+  Which is very exotic, and I think never encountered; but see
+  Note [Equality superclasses in quantified constraints]
+  in TcCanonical
+
 Note [CoreSyn case invariants]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 See #case_invariants#
@@ -2102,6 +2117,12 @@ isTyCoArg (Type {})     = True
 isTyCoArg (Coercion {}) = True
 isTyCoArg _             = False
 
+-- | Returns @True@ iff the expression is a 'Coercion'
+-- expression at its top level
+isCoArg :: Expr b -> Bool
+isCoArg (Coercion {}) = True
+isCoArg _             = False
+
 -- | Returns @True@ iff the expression is a 'Type' expression at its
 -- top level.  Note this does NOT include 'Coercion's.
 isTypeArg :: Expr b -> Bool
diff --git a/compiler/coreSyn/CoreUtils.hs b/compiler/coreSyn/CoreUtils.hs
index 3c65072974..7635a6d66a 100644
--- a/compiler/coreSyn/CoreUtils.hs
+++ b/compiler/coreSyn/CoreUtils.hs
@@ -481,8 +481,15 @@ bindNonRec :: Id -> CoreExpr -> CoreExpr -> CoreExpr
 -- the simplifier deals with them perfectly well. See
 -- also 'MkCore.mkCoreLet'
 bindNonRec bndr rhs body
-  | needsCaseBinding (idType bndr) rhs = Case rhs bndr (exprType body) [(DEFAULT, [], body)]
-  | otherwise                          = Let (NonRec bndr rhs) body
+  | isTyVar bndr                       = let_bind
+  | isCoVar bndr                       = if isCoArg rhs then let_bind
+    {- See Note [Binding coercions] -}                  else case_bind
+  | isJoinId bndr                      = let_bind
+  | needsCaseBinding (idType bndr) rhs = case_bind
+  | otherwise                          = let_bind
+  where
+    case_bind = Case rhs bndr (exprType body) [(DEFAULT, [], body)]
+    let_bind  = Let (NonRec bndr rhs) body
 
 -- | Tests whether we have to use a @case@ rather than @let@ binding for this expression
 -- as per the invariants of 'CoreExpr': see "CoreSyn#let_app_invariant"
@@ -505,7 +512,12 @@ mkAltExpr (LitAlt lit) [] []
 mkAltExpr (LitAlt _) _ _ = panic "mkAltExpr LitAlt"
 mkAltExpr DEFAULT _ _ = panic "mkAltExpr DEFAULT"
 
-{-
+{- Note [Binding coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider binding a CoVar, c = e.  Then, we must atisfy
+Note [CoreSyn type and coercion invariant] in CoreSyn,
+which allows only (Coercion co) on the RHS.
+
 ************************************************************************
 *                                                                      *
                Operations oer case alternatives
diff --git a/compiler/coreSyn/MkCore.hs b/compiler/coreSyn/MkCore.hs
index c3b1625333..a425ad249e 100644
--- a/compiler/coreSyn/MkCore.hs
+++ b/compiler/coreSyn/MkCore.hs
@@ -107,9 +107,7 @@ sortQuantVars vs = sorted_tcvs ++ ids
 -- appropriate (see "CoreSyn#let_app_invariant")
 mkCoreLet :: CoreBind -> CoreExpr -> CoreExpr
 mkCoreLet (NonRec bndr rhs) body        -- See Note [CoreSyn let/app invariant]
-  | needsCaseBinding (idType bndr) rhs
-  , not (isJoinId bndr)
-  = Case rhs bndr (exprType body) [(DEFAULT,[],body)]
+  = bindNonRec bndr rhs body
 mkCoreLet bind body
   = Let bind body
 
diff --git a/compiler/simplCore/Simplify.hs b/compiler/simplCore/Simplify.hs
index 1041bc13cc..872973925f 100644
--- a/compiler/simplCore/Simplify.hs
+++ b/compiler/simplCore/Simplify.hs
@@ -44,6 +44,7 @@ import Demand           ( mkClosedStrictSig, topDmd, exnRes )
 import BasicTypes       ( TopLevelFlag(..), isNotTopLevel, isTopLevel,
                           RecFlag(..), Arity )
 import MonadUtils       ( mapAccumLM, liftIO )
+import Var              ( isTyCoVar )
 import Maybes           (  orElse )
 import Control.Monad
 import Outputable
@@ -2425,9 +2426,7 @@ rebuildCase env scrut case_bndr alts@[(_, bndrs, rhs)] cont
   --           lifted case: the scrutinee is in HNF (or will later be demanded)
   -- See Note [Case to let transformation]
   | all_dead_bndrs
-  , if isUnliftedType (idType case_bndr)
-    then exprOkForSpeculation scrut
-    else exprIsHNF scrut || case_bndr_is_demanded
+  , doCaseToLet scrut case_bndr
   = do { tick (CaseElim case_bndr)
        ; (floats1, env') <- simplNonRecX env case_bndr scrut
        ; (floats2, expr') <- simplExprF env' rhs cont
@@ -2446,12 +2445,27 @@ rebuildCase env scrut case_bndr alts@[(_, bndrs, rhs)] cont
     all_dead_bndrs = all isDeadBinder bndrs       -- bndrs are [InId]
     is_plain_seq   = all_dead_bndrs && isDeadBinder case_bndr -- Evaluation *only* for effect
 
-    case_bndr_is_demanded = isStrictDmd (idDemandInfo case_bndr)
-    -- See Note [Case-to-let for strictly-used binders]
-
 rebuildCase env scrut case_bndr alts cont
   = reallyRebuildCase env scrut case_bndr alts cont
 
+
+doCaseToLet :: OutExpr          -- Scrutinee
+            -> InId             -- Case binder
+            -> Bool
+-- The situation is         case scrut of b { DEFAULT -> body }
+-- Can we transform thus?   let { b = scrut } in body
+doCaseToLet scrut case_bndr
+  | isTyCoVar case_bndr    -- Respect CoreSyn
+  = isTyCoArg scrut        -- Note [CoreSyn type and coercion invariant]
+
+  | isUnliftedType (idType case_bndr)
+  = exprOkForSpeculation scrut
+
+  | otherwise  -- Scrut has a lifted type
+  = exprIsHNF scrut
+    || isStrictDmd (idDemandInfo case_bndr)
+    -- See Note [Case-to-let for strictly-used binders]
+
 --------------------------------------------------
 --      3. Catch-all case
 --------------------------------------------------
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index b9b59d121f..3ff54dff5c 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -23,6 +23,7 @@ import TcEvTerm
 import Class
 import TyCon
 import TyCoRep   -- cleverly decomposes types, good for completeness checking
+import TysWiredIn( cTupleTyConName )
 import Coercion
 import CoreSyn
 import Id( idType, mkTemplateLocals )
@@ -487,16 +488,31 @@ mk_strict_superclasses rec_clss ev tvs theta cls tys
     size      = sizeTypes tys
 
     do_one_given evar given_loc sel_id
-      = do { let sc_pred = funResultTy (piResultTys (idType sel_id) tys)
-                 given_ty = mkInfSigmaTy tvs theta sc_pred
-           ; given_ev <- newGivenEvVar given_loc $
-                         (given_ty, mk_sc_sel evar sel_id)
+      | not (null tvs)
+      , null theta
+      , isUnliftedType sc_pred
+      -- Very special case for equality
+      -- See Note [Equality superclasses in quantified constraints]
+      = do { empty_ctuple_cls <- tcLookupClass (cTupleTyConName 0)
+           ; let theta1    = [mkClassPred empty_ctuple_cls []]
+                 dict_ids1 = mkTemplateLocals theta1
+           ; given_ev <- new_given theta1 dict_ids1 []
+           ; return [mkNonCanonical given_ev] }
+
+      | otherwise  -- Normal case
+      = do { given_ev <- new_given theta dict_ids dict_ids
            ; mk_superclasses rec_clss given_ev tvs theta sc_pred }
 
-    mk_sc_sel evar sel_id
-      = EvExpr $ mkLams tvs $ mkLams dict_ids $
-        Var sel_id `mkTyApps` tys `App`
-        (evId evar `mkTyApps` mkTyVarTys tvs `mkVarApps` dict_ids)
+      where
+        sc_pred = funResultTy (piResultTys (idType sel_id) tys)
+
+        new_given theta_abs dict_ids_abs dict_ids_app
+          = newGivenEvVar given_loc (given_ty, given_ev)
+          where
+            given_ty = mkInfSigmaTy tvs theta_abs sc_pred
+            given_ev = EvExpr $ mkLams tvs $ mkLams dict_ids_abs $
+                       Var sel_id `mkTyApps` tys `App`
+                       (evId evar `mkTyApps` mkTyVarTys tvs `mkVarApps` dict_ids_app)
 
     mk_given_loc loc
        | isCTupleClass cls
@@ -574,7 +590,45 @@ mk_superclasses_of rec_clss ev tvs theta cls tys
                              , qci_pend_sc = loop_found })
 
 
-{-
+{- Note [Equality superclasses in quantified constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (Trac #15359, #15593, #15625)
+  f :: (forall a. theta => a ~ b) => stuff
+
+It's a bit odd to have a local, quantified constraint for `(a~b)`,
+but some people want such a thing (see the tickets). And for
+Coercible it is definitely useful
+  f :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q)))
+                 => stuff
+
+Moreover it's not hard to arrange; we just need to look up /equality/
+constraints in the quantified-constraint environment, which we do in
+TcInteract.doTopReactOther.
+
+There is a wrinkle though, in the case where 'theta' is empty, so
+we have
+  f :: (forall a. a~b) => stuff
+
+Now the superclass machinery kicks in, in makeSuperClasses,
+giving us a a second quantified constrait
+       (forall a. a ~# b)
+BUT this is an unboxed value!  And nothing has prepared us for
+dictionary "functions" that are unboxed.  Actually it does just
+about work, but the simplier ends up with stuff like
+   case (/\a. eq_sel d) of df -> ...(df @Int)...
+and fails to simplify that any further.
+
+It seems eaiser to give such unboxed quantifed constraints a
+dummmy () argument, thus
+      (forall a. (% %) => a ~# b)
+where (% %) is the empty constraint tuple.  That makes everything
+be nicely boxed.
+
+(One might wonder about using void# instead, but this seems more
+uniform -- it's a constraint argument -- and I'm not worried about
+the last drop of efficiency for this very rare case.)
+
+
 ************************************************************************
 *                                                                      *
 *                      Irreducibles canonicalization
@@ -2013,7 +2067,7 @@ canEqTyVarTyVar, are these
    gets eliminated (improves error messages)
 
  * If one is a flatten-skolem, put it on the left so that it is
-   substituted out  Note [Elminate flat-skols]
+   substituted out  Note [Eliminate flat-skols] in TcUinfy
         fsk ~ a
 
 Note [Equalities with incompatible kinds]
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 028b755187..1771e19849 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -1820,9 +1820,14 @@ topReactionsStage work_item
 
 --------------------
 doTopReactOther :: Ct -> TcS (StopOrContinue Ct)
+-- Try local quantified constraints for
+--     CTyEqCan  e.g.  (a ~# ty)
+-- and CIrredCan e.g.  (c a)
+--
+-- Why equalities? See TcCanonical
+-- Note [Equality superclasses in quantified constraints]
 doTopReactOther work_item
-  = do { -- Try local quantified constraints
-         res <- matchLocalInst pred (ctEvLoc ev)
+  = do { res <- matchLocalInst pred (ctEvLoc ev)
        ; case res of
            OneInst {} -> chooseInstance work_item res
            _          -> continueWith work_item }
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 2fde421f79..b58c1ba74e 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -1142,21 +1142,14 @@ check_valid_inst_head dflags this_mod is_boot ctxt clas cls_args
   , hand_written_bindings
   = failWithTc rejected_class_msg
 
-  -- For the most part we don't allow instances for Coercible;
+  -- For the most part we don't allow
+  -- instances for (~), (~~), or Coercible;
   -- but we DO want to allow them in quantified constraints:
   --   f :: (forall a b. Coercible a b => Coercible (m a) (m b)) => ...m...
-  | clas_nm == coercibleTyConName
+  | clas_nm `elem` [ heqTyConName, eqTyConName, coercibleTyConName ]
   , not quantified_constraint
   = failWithTc rejected_class_msg
 
-  -- Handwritten instances of other nonminal-equality classes
-  -- is forbidden, except in the defining module to allow
-  --    instance a ~~ b => a ~ b
-  -- which occurs in Data.Type.Equality
-  | clas_nm `elem` [ heqTyConName, eqTyConName]
-  , nameModule clas_nm /= this_mod
-  = failWithTc rejected_class_msg
-
   -- Check for hand-written Generic instances (disallowed in Safe Haskell)
   | clas_nm `elem` genericClassNames
   , hand_written_bindings
diff --git a/testsuite/tests/quantified-constraints/T15359.hs b/testsuite/tests/quantified-constraints/T15359.hs
new file mode 100644
index 0000000000..7ef1cc5572
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15359.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE MultiParamTypeClasses, GADTs, RankNTypes,
+             ConstraintKinds, QuantifiedConstraints #-}
+
+module T15359 where
+
+class C a b
+
+data Dict c where
+  Dict :: c => Dict c
+
+foo :: (forall a b. C a b => a ~ b) => Dict (C a b) -> a -> b
+foo Dict x = x
diff --git a/testsuite/tests/quantified-constraints/T15359a.hs b/testsuite/tests/quantified-constraints/T15359a.hs
new file mode 100644
index 0000000000..6ec5f861a8
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15359a.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE MultiParamTypeClasses, GADTs, RankNTypes,
+             ConstraintKinds, QuantifiedConstraints,
+             UndecidableInstances #-}
+
+module T15359a where
+
+class C a b
+class a ~ b => D a b
+
+data Dict c where
+  Dict :: c => Dict c
+
+foo :: (forall a b. C a b => D a b) => Dict (C a b) -> a -> b
+foo Dict x = x
diff --git a/testsuite/tests/quantified-constraints/T15625.hs b/testsuite/tests/quantified-constraints/T15625.hs
new file mode 100644
index 0000000000..8fe092da98
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15625.hs
@@ -0,0 +1,16 @@
+{-# Language GADTs, MultiParamTypeClasses, QuantifiedConstraints #-}
+
+module T15625 where
+
+import Data.Coerce
+
+class a ~ b => Equal a b
+
+test1 :: (forall b. a ~ b) => a
+test1 = False
+
+test2 :: (forall b. Equal a b) => a
+test2 = False
+
+test3 :: (forall b. Coercible a b) => a
+test3 = coerce False
diff --git a/testsuite/tests/quantified-constraints/T15625a.hs b/testsuite/tests/quantified-constraints/T15625a.hs
new file mode 100644
index 0000000000..ca049cb19d
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15625a.hs
@@ -0,0 +1,20 @@
+{-# Language RankNTypes, ConstraintKinds, QuantifiedConstraints,
+             PolyKinds, GADTs, MultiParamTypeClasses,
+             DataKinds, FlexibleInstances #-}
+
+module T15625a where
+
+import Data.Kind
+
+type Cat ob = ob -> ob -> Type
+
+data KLEISLI (m :: Type -> Type) :: Cat (KL_kind m) where
+  MkKLEISLI :: (a -> m b) -> KLEISLI(m) (KL a) (KL b)
+
+data KL_kind (m :: Type -> Type) = KL Type
+
+class    (a ~ KL xx) => AsKL a xx
+instance (a ~ KL xx) => AsKL a xx
+
+ekki__ :: Monad m => (forall xx. AsKL a xx) => KLEISLI m a a
+ekki__ = MkKLEISLI undefined
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
index 833a667ea9..1e2eca8358 100644
--- a/testsuite/tests/quantified-constraints/all.T
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -16,3 +16,7 @@ test('T15290a', normal, compile_fail, [''])
 test('T15290b', normal, compile_fail, [''])
 test('T15316', normal, compile_fail, [''])
 test('T15334', normal, compile_fail, [''])
+test('T15359', normal, compile, [''])
+test('T15359a', normal, compile, [''])
+test('T15625', normal, compile, [''])
+test('T15625a', normal, compile, [''])