summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2018-09-13 11:23:53 +0100
committerSimon Peyton Jones <simonpj@microsoft.com>2018-09-13 11:35:00 +0100
commitbd76875ae6ad0cdd734564dddfb9ab88a6de9579 (patch)
treedddaeaf707a06f3e4b34d462978a20f89c12b0f6
parent291b0f89703f28631a381549e1838aa06195d011 (diff)
downloadhaskell-bd76875ae6ad0cdd734564dddfb9ab88a6de9579.tar.gz
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],
-rw-r--r--compiler/coreSyn/CoreLint.hs6
-rw-r--r--compiler/coreSyn/CoreOpt.hs35
-rw-r--r--compiler/coreSyn/CoreSyn.hs71
-rw-r--r--compiler/coreSyn/CoreUtils.hs18
-rw-r--r--compiler/coreSyn/MkCore.hs4
-rw-r--r--compiler/simplCore/Simplify.hs26
-rw-r--r--compiler/typecheck/TcCanonical.hs74
-rw-r--r--compiler/typecheck/TcInteract.hs9
-rw-r--r--compiler/typecheck/TcValidity.hs13
-rw-r--r--testsuite/tests/quantified-constraints/T15359.hs12
-rw-r--r--testsuite/tests/quantified-constraints/T15359a.hs14
-rw-r--r--testsuite/tests/quantified-constraints/T15625.hs16
-rw-r--r--testsuite/tests/quantified-constraints/T15625a.hs20
-rw-r--r--testsuite/tests/quantified-constraints/all.T4
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, [''])