Opened 7 months ago
Closed 6 months ago
#15290 closed bug (fixed)
QuantifiedConstraints: panic "addTcEvBind NoEvBindsVar"
Reported by:  goldfire  Owned by:  

Priority:  normal  Milestone:  8.6.1 
Component:  Compiler  Version:  8.4.3 
Keywords:  QuantifiedConstraints  Cc:  
Operating System:  Unknown/Multiple  Architecture:  Unknown/Multiple 
Type of failure:  None/Unknown  Test Case:  quantifiedconstraints/T15290{,a,b}, deriving/should_compile/T15290{c,d}, deriving/should_compile/T14883 
Blocked By:  Blocking:  
Related Tickets:  Differential Rev(s):  Phab:D4895  
Wiki Page: 
Description
I wanted to see if we're ready to put join
into Monad
. So I typed this in:
{# LANGUAGE QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #} module Bug where import Prelude hiding ( Monad(..) ) import Data.Coerce ( Coercible ) class Monad m where (>>=) :: m a > (a > m b) > m b join :: m (m a) > m a newtype StateT s m a = StateT { runStateT :: s > m (s, a) } instance Monad m => Monad (StateT s m) where ma >>= fmb = StateT $ \s > runStateT ma s >>= \(s1, a) > runStateT (fmb a) s1 join ssa = StateT $ \s > runStateT ssa s >>= \(s, sa) > runStateT sa s newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a } deriving instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q)) => Monad (IntStateT m)
This looks like it should be accepted. But I get
ghcstage2: panic! (the 'impossible' happened) (GHC version 8.5.20180617 for x86_64appledarwin): addTcEvBind NoEvBindsVar [G] df_a67k = \ (@ p_a62C) (@ q_a62D) (v_B1 :: Coercible p_a62C q_a62D) > coercible_sel @ * @ (m_a64Z[ssk:1] p_a62C) @ (m_a64Z[ssk:1] q_a62D) (df_a651 @ p_a62C @ q_a62D v_B1) a67c Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable pprPanic, called at compiler/typecheck/TcRnMonad.hs:1404:5 in ghc:TcRnMonad
Change History (39)
comment:1 Changed 7 months ago by
comment:3 Changed 7 months ago by
Blocking:  9123 added 

comment:4 Changed 7 months ago by
Blocking:  14883 added 

comment:5 Changed 7 months ago by
Good grief. At first I thought the problem was simple, but now I realise there is more to it than that.
Here is a minimised version that crashes
{# LANGUAGE TypeApplications, ImpredicativeTypes, ScopedTypeVariables, QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #} module T15290 where import Prelude hiding ( Monad(..) ) import Data.Coerce ( Coercible, coerce ) class Monad m where join :: m (m a) > m a newtype StateT s m a = StateT { runStateT :: s > m (s, a) } newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a } instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q)) => Monad (IntStateT m) where join = coerce @(forall a. StateT Int m (StateT Int m a) > StateT Int m a) @(forall a. IntStateT m (IntStateT m a) > IntStateT m a) join
The deriving
mechanism tries to instantiate coerce
at a polymorphic type,
a form of impredicative polymorphism, so it's on thin ice. And in fact
the ice breaks.
The call to coerce
gives rise to
Coercible (forall a. blah1) (forall a. blah2)
and that soon simplifies to the implication constraint (because of the forall)
forall a <noev>. m (Int, IntStateT m a) ~R# m (Int, StateT Int m a)
But, becuase this constraint is under a forall, inside a type, we have
to prove it without computing any term evidence. Hence the <noev>
,
meaning I can't generate any termlevel evidence bindings.
Alas, I must generate a termlevel evidence binding, to instantiate the quantified constraint. Currently GHC crashes, but I suppose it should instead decline to consult given quantified constraints if it's in a context where evidence bindings are not allowed. I don't see any way out here.
All this arises from a sneaky attempt to use impredicative polymorphism. Maybe instead the derviing mechansim should generate
join = (coerce @(StateT Int m (StateT Int m a) > StateT Int m a) @(IntStateT m (IntStateT m a) > IntStateT m a) join) :: forall a. IntStateT m (IntStateT m a) > IntStateT m a
and use ordinary predicative instantiation for coerce
. And
indeed that works fine right now. It'll mean a bit more work for
the deriving
mechanism, but not much.
Richard and Ryan may want to comment.
comment:6 Changed 7 months ago by
I don't think your workaround is sufficient to avoid the issue. Consider what would happen if we had a variant of join
with this type signature:
join :: (forall b. b > a) > m (m a) > m a
If we plug that in to our proposed scheme:
{# LANGUAGE TypeApplications, ImpredicativeTypes, ScopedTypeVariables, QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #} module T15290 where import Prelude hiding ( Monad(..) ) import Data.Coerce ( Coercible, coerce ) class Monad m where join :: (forall b. b > a) > m (m a) > m a newtype StateT s m a = StateT { runStateT :: s > m (s, a) } instance Monad m => Monad (StateT s m) where newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a } instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q)) => Monad (IntStateT m) where join = coerce @((forall b. b > a) > StateT Int m (StateT Int m a) > StateT Int m a) @((forall b. b > a) > IntStateT m (IntStateT m a) > IntStateT m a) join :: forall a. (forall b. b > a) > IntStateT m (IntStateT m a) > IntStateT m a
Then that, too, will panic:
$ /opt/ghc/head/bin/ghc Bug.hs [1 of 1] Compiling T15290 ( Bug.hs, Bug.o ) ghc: panic! (the 'impossible' happened) (GHC version 8.5.20180616 for x86_64unknownlinux): addTcEvBind NoEvBindsVar [G] df_a1pg = \ (@ p_aW5) (@ q_aW6) (v_B1 :: Coercible p_aW5 q_aW6) > coercible_sel @ * @ (m_a1nx[ssk:1] p_aW5) @ (m_a1nx[ssk:1] q_aW6) (df_a1nz @ p_aW5 @ q_aW6 v_B1) a1og Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable pprPanic, called at compiler/typecheck/TcRnMonad.hs:1404:5 in ghc:TcRnMonad
comment:7 Changed 7 months ago by
Yes, I agree. I can (and will) stop the panic (by refraining from using quantified constraints if I have no place to put the evidence) but that will make GHC reject deriving
for
 A higher rank method
 That makes essential use of a quantified constraint
 Under a forall
I don't see how to avoid that restriction. If anyone else does, please say so!
comment:8 Changed 7 months ago by
Wait, you're saying that deriving classes with methods that use higherrank types will no longer work? If so, that is going to break enormous swaths of code both in the wild and in the test suite (see here for one example).
comment:9 Changed 7 months ago by
Wait, you're saying that deriving classes with methods that use higherrank types will no longer work?
No, I am not saying that (see the second bullet). It's just that if you can't simultaneously exploit impredicative instantiation of coerce
and quantified constraints.
comment:10 Changed 7 months ago by
Ah, my apologies. I interpreted that list of bullet points as three separate criteria under which deriving
would fail, not as a list of three conditions which must simultaneously hold.
In that case, I feel much better about this idea (if this really is the only way forward). I've always thought that derived instance methods should use InstanceSigs
, and this gives us a good excuse to do so. (And I think certain folks, possibly from Iceland, will find that more aesthetically pleasing to look at in ddumpderiv
output.)
comment:11 Changed 7 months ago by
You could use InstanceSigs
; or just an expression type signature as I have done.
And incidentally you can them omit the second type argument to coerce
, which is perhaps nice.
comment:12 Changed 7 months ago by
To be clear: are you working on the change to deriving
alongside the typechecker changes? Or should I implement the deriving
bits?
comment:15 Changed 7 months ago by
Hm, I've hit a roadblock when trying to switch over to the scheme proposed in comment:5. Consider this code:
{# LANGUAGE GeneralizedNewtypeDeriving #} {# LANGUAGE ImpredicativeTypes #} {# LANGUAGE KindSignatures #} {# LANGUAGE RankNTypes #} {# LANGUAGE ScopedTypeVariables #} {# LANGUAGE TypeApplications #} {# OPTIONS_GHC ddumpderiv #} module Bug where import Data.Coerce class C a where c :: Int > forall b. b > a instance C Int where c _ _ = 42 newtype Age = MkAge Int  This is what   deriving instance C Age   would generate: instance C Age where c = coerce @( Int > forall b. b > Int) c :: Int > forall b. b > Age
This fails to typecheck:
$ /opt/ghc/8.4.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:26:7: error: • Couldn't match representation of type ‘forall b2. b2 > Int’ with that of ‘b1 > Age’ arising from a use of ‘coerce’ • In the expression: coerce @(Int > forall b. b > Int) c :: Int > forall b. b > Age In an equation for ‘c’: c = coerce @(Int > forall b. b > Int) c :: Int > forall b. b > Age In the instance declaration for ‘C Age’  26  c = coerce @( Int > forall b. b > Int)  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
The same error occurs if I use InstanceSigs
.
Any ideas on how to make this work?
comment:16 Changed 7 months ago by
The current behavior was introduced in b612da667fe8fa5277fc78e972a86d4b35f98364
That commit fixes some impredicativity bug but also rewrites GND to use type application. However, the change to GND also has it work with polytypes instead of its previous behavior, using monotypes. It sounds like we want to go to the previous behavior.
As for Ryan's question: try passing both type arguments to coerce
. As explained in the visible type application paper, type signatures on expressions are deeply skolemized, which is causing havoc for you here. I think including the second type parameter to coerce
will solve the problem.
comment:17 Changed 7 months ago by
Thanks Richard, that did indeed solve that problem.
On the other hand, I seem to have hit an even trickier problem. For context: this is the entirety of my patch at the moment:

compiler/typecheck/TcGenDeriv.hs
diff git a/compiler/typecheck/TcGenDeriv.hs b/compiler/typecheck/TcGenDeriv.hs index b944520..1f1cba2 100644
a b gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty 1668 1668 [] rhs_expr] 1669 1669 where 1670 1670 Pair from_ty to_ty = mkCoerceClassMethEqn cls inst_tvs inst_tys rhs_ty meth_id 1671 (_, _, from_tau) = tcSplitSigmaTy from_ty 1672 (_, _, to_tau) = tcSplitSigmaTy to_ty 1671 1673 1672 1674 meth_RDR = getRdrName meth_id 1673 1675 1674 1676 rhs_expr = nlHsVar (getRdrName coerceId) 1675 `nlHsAppType` from_ty 1676 `nlHsAppType` to_ty 1677 `nlHsApp` nlHsVar meth_RDR 1677 `nlHsAppType` from_tau 1678 `nlHsAppType` to_tau 1679 `nlHsApp` nlHsVar meth_RDR 1680 `nlExprWithTySig` to_ty 1678 1681 1679 1682 mk_atf_inst :: TyCon > TcM FamInst 1680 1683 mk_atf_inst fam_tc = do
i.e., drop the forall
s from each of the types inside the explicit type applications, and put an explicit type signature (with forall
s) on the whole expression.
Now here's the kicker: if you try that patch on this program:
{# LANGUAGE GeneralizedNewtypeDeriving #} {# LANGUAGE ScopedTypeVariables #} {# LANGUAGE TypeApplications #} {# OPTIONS_GHC ddumpderiv #} module Bug where import Data.Coerce class Foo a where bar :: a > Maybe b instance Foo Int where bar _ = Nothing newtype Age = MkAge Int deriving Foo
Then it no longer typechecks:
$ inplace/bin/ghcstage2 interactive ../Bug2.hs GHCi, version 8.7.20180621: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( ../Bug2.hs, interpreted ) ==================== Derived instances ==================== Derived class instances: instance Bug.Foo Bug.Age where Bug.bar = GHC.Prim.coerce @(GHC.Types.Int > GHC.Maybe.Maybe b_a1AR) @(Bug.Age > GHC.Maybe.Maybe b_a1AR) Bug.bar :: forall (b_a1AR :: TYPE GHC.Types.LiftedRep). Bug.Age > GHC.Maybe.Maybe b_a1AR Derived type family instances: ../Bug2.hs:16:12: error: • Couldn't match type ‘b1’ with ‘b’ ‘b1’ is a rigid type variable bound by an expression type signature: forall b1. Age > Maybe b1 at ../Bug2.hs:16:1214 ‘b’ is a rigid type variable bound by the type signature for: bar :: forall b. Age > Maybe b at ../Bug2.hs:16:1214 Expected type: Age > Maybe b1 Actual type: Age > Maybe b • In the expression: coerce @(Int > Maybe b) @(Age > Maybe b) bar :: forall (b :: TYPE GHC.Types.LiftedRep). Age > Maybe b In an equation for ‘bar’: bar = coerce @(Int > Maybe b) @(Age > Maybe b) bar :: forall (b :: TYPE GHC.Types.LiftedRep). Age > Maybe b When typechecking the code for ‘bar’ in a derived instance for ‘Foo Age’: To see the code I am typechecking, use ddumpderiv In the instance declaration for ‘Foo Age’ • Relevant bindings include bar :: Age > Maybe b (bound at ../Bug2.hs:16:12)  16  deriving Foo  ^^^
For the life of me, I can't figure out why this shouldn't typecheck. What's even stranger, if I take the code that GHC's giving me and paste it back into the source:
{# LANGUAGE GeneralizedNewtypeDeriving #} {# LANGUAGE ScopedTypeVariables #} {# LANGUAGE TypeApplications #} {# OPTIONS_GHC ddumpderiv #} module Bug where import Data.Coerce class Foo a where bar :: a > Maybe b instance Foo Int where bar _ = Nothing newtype Age = MkAge Int  deriving Foo instance Foo Age where bar = coerce @(Int > Maybe b) @(Age > Maybe b) bar :: forall b. Age > Maybe b
Then it typechecks again!
comment:19 Changed 7 months ago by
Test Case:  → quantifiedconstraints/T15290, T15290a 

comment:20 Changed 7 months ago by
To make things more outrageous, if I manually freshen the type variable binders in to_ty
in comment:17 (using freshTyVarBndrs
), then it works. Quite mysterious.
comment:22 Changed 7 months ago by
On the subject of the actual panic observed in this ticket, I don't think Simon's commit quite fixed it. I'm still observing the panic on commit 122ba98af22c2b016561433dfa55bbabba98d972 with this program (taken from #14883):
{# LANGUAGE ConstraintKinds #} {# LANGUAGE ImpredicativeTypes #} {# LANGUAGE InstanceSigs #} {# LANGUAGE KindSignatures #} {# LANGUAGE GeneralizedNewtypeDeriving #} {# LANGUAGE QuantifiedConstraints #} {# LANGUAGE RankNTypes #} {# LANGUAGE ScopedTypeVariables #} {# LANGUAGE TypeApplications #} module Bug where import Data.Coerce import Data.Kind type Representational1 m = (forall a b. Coercible a b => Coercible (m a) (m b) :: Constraint) class Representational1 f => Functor' f where fmap' :: (a > b) > f a > f b class Functor' f => Applicative' f where pure' :: a > f a (<*>@) :: f (a > b) > f a > f b class Functor' t => Traversable' t where traverse' :: Applicative' f => (a > f b) > t a > f (t b)  Typechecks newtype T1 m a = MkT1 (m a) deriving (Functor', Traversable')
$ ghc/inplace/bin/ghcstage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) ghcstage2: panic! (the 'impossible' happened) (GHC version 8.7.20180621 for x86_64unknownlinux): addTcEvBind NoEvBindsVar [G] df_a1bF = \ (@ a_asM) (@ b_asN) (v_B1 :: Coercible a_asM b_asN) > coercible_sel @ * @ (m_a1bn[sk:1] a_asM) @ (m_a1bn[sk:1] b_asN) (df_a1bE @ a_asM @ b_asN v_B1) a1bw Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable pprPanic, called at compiler/typecheck/TcRnMonad.hs:1404:5 in ghc:TcRnMonad
The panic does not occur if I derive Traversable'
through StandaloneDeriving
.
comment:23 Changed 7 months ago by
Replying to simonpj:
I'm on it. Digging through manure in
TcHsType
.
Presumably mine. What's up this time? :)
comment:24 Changed 7 months ago by
Good grief  again! comment:17 is ghastly. Here's what is happening. What we are 'really' checking is
bar = ((coerce @(Int > Maybe b) @(Age > Maybe b) bar) :: forall b. Age > Maybe b) :: forall b. Age > Maybe b
where
 the outer type signature comes from checking that the type of the method matches the type that the class expects
 the inner one comes from the 'deriving' patch
Because both of those type sigs ultimately from the same source, both 'b's happen to have the same unique. That should be fine but it isn't:
 The outer forall adds
b :> b1[sk]
to the type environment. That's fine, even though this outer forall b does not scope; the type envt isn't responsible for resolving lexical scoping.
 The
forall
on the inner signature is typechecked with by theHsForAllTy
case oftc_hs_type
, which callstcExplicitTKBndrs
, which callstcHsTyVarBndr
, which callstcHsTyVarName
, which has a special case for type variables already in scope
 The inscope handling in
tcHsTyVarName
is a very special case intended only for the binders in theLHSQTyVars
of an associated type or type instance declaration, nested inside a class decl. Yet it is here being used (accidentally) for theforall
of a type signature, a situation that it is utterly unsuitable for. Even if the tyvar for aforall
is already in scope, that should be utterly irrelevant to the type signature.
 The net result is chaos: we end up with two different skolems that really represent the same type variable.
Conclusion: we should radically narrow the cases in which this funny inscope test applies.
comment:25 Changed 7 months ago by
Simon made a commit (9fc40c733ba8822a04bd92883801b214dee099ca) addressing the issue in comment:24, but he accidentally tagged the wrong ticket number. Here is the commit:
From 9fc40c733ba8822a04bd92883801b214dee099ca Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones <simonpj@microsoft.com> Date: Mon, 25 Jun 2018 13:20:59 +0100 Subject: [PATCH] Refactor the kindchecking of tyvar binders The refactoring here is driven by the ghastly mess described in comment:24 of Trac #1520. The overall goal is to simplify the kindchecking of typevvariable binders, and in particular to narrow the use of the "inscope tyvar binder" stuff, which is needed only for associated types: see the new Note [Kindchecking tyvar binders for associated types] in TcHsType. Now * The "inscope tyvar binder" stuff is done only in  kcLHsQTyVars, which is used for the LHsQTyVars of a data/newtype, or type family declaration.  tcFamTyPats, which is used for associated family instances; it now calls tcImplicitQTKBndrs, which in turn usese newFlexiKindedQTyVar * tcExpicitTKBndrs (which is used only for function signatures, data con signatures, pattern synonym signatures, and expression type signatures) now does not go via the "inscope tyvar binder" stuff at all. While I'm still not happy with all this code, the code is generally simpler, and I think this is a useful step forward. It does cure the problem too. (It's hard to trigger the problem in vanilla Haskell code, because the renamer would normally use different names for nested binders, so I can't offer a test.)  compiler/hsSyn/HsDecls.hs  43 +++++ compiler/typecheck/TcHsType.hs  258 +++++++++++++++++++++ compiler/typecheck/TcTyClsDecls.hs  3 + 3 files changed, 178 insertions(+), 126 deletions()
comment:26 Changed 7 months ago by
Thanks for putting this in the right place. I think your patch should work now; and I tried this which seems even better
diff git a/compiler/typecheck/TcGenDeriv.hs b/compiler/typecheck/TcGenDeriv.hs index b944520..736eb14 100644  a/compiler/typecheck/TcGenDeriv.hs +++ b/compiler/typecheck/TcGenDeriv.hs @@ 1668,13 +1668,12 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty [] rhs_expr] where Pair from_ty to_ty = mkCoerceClassMethEqn cls inst_tvs inst_tys rhs_ty meth_id  meth_RDR = getRdrName meth_id + (_, _, from_tau) = tcSplitSigmaTy from_ty rhs_expr = nlHsVar (getRdrName coerceId)  `nlHsAppType` from_ty  `nlHsAppType` to_ty  `nlHsApp` nlHsVar meth_RDR + `nlHsApp` (nlHsVar meth_RDR `nlExprWithTySig` from_tau) + `nlExprWithTySig` to_ty mk_atf_inst :: TyCon > TcM FamInst mk_atf_inst fam_tc = do @@ 1703,11 +1702,6 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty rep_cvs' = toposortTyVars rep_cvs pp_lhs = ppr (mkTyConApp fam_tc rep_lhs_tys) nlHsAppType :: LHsExpr GhcPs > Type > LHsExpr GhcPs nlHsAppType e s = noLoc (HsAppType hs_ty e)  where  hs_ty = mkHsWildCardBndrs $ nlHsParTy (typeToLHsType s)  nlExprWithTySig :: LHsExpr GhcPs > Type > LHsExpr GhcPs nlExprWithTySig e s = noLoc $ ExprWithTySig hs_ty $ parenthesizeHsExpr sigPrec e
I like this because it feels more uniform: two type signatures rather that one type signature and two type applications.
Validate goes through (I think) except for ddumpderiv
output. Over to you on that front.
comment:27 Changed 7 months ago by
Thanks, Simon.
Do be aware that the program in comment:22 still panics. I'll check that it as an expect_broken
test case in my upcoming patch.
comment:28 Changed 7 months ago by
On the subject of the actual panic observed in this ticket, I don't think Simon's commit quite fixed it. I'm still observing the panic on commit 122ba98af22c2b016561433dfa55bbabba98d972 with this program (taken from #14883):
Ah, correction, I can reproduce this. Weird. I'll look.
comment:29 Changed 7 months ago by
Actually, it turns out that the approach in comment:26 isn't feasible. It breaks on the program in comment:15, as it generates the following code:
{# LANGUAGE GeneralizedNewtypeDeriving #} {# LANGUAGE RankNTypes #} {# LANGUAGE ScopedTypeVariables #} {# LANGUAGE TypeApplications #} module T15290b where import Data.Coerce class C a where c :: Int > forall b. b > a instance C Int where c _ _ = 42 newtype Age = MkAge Int  deriving C instance C Age where c = coerce (c :: Int > forall b. b > Int) :: Int > forall b. b > Age
$ ghc Bug.hs [1 of 1] Compiling T15290b ( Bug.hs, Bug.o ) Bug.hs:19:7: error: • Couldn't match representation of type ‘b0’ with that of ‘b1’ arising from a use of ‘coerce’ ‘b1’ is a rigid type variable bound by a type expected by the context: Int > forall b1. b1 > Age at Bug.hs:19:5074 • In the expression: coerce (c :: Int > forall b. b > Int) :: Int > forall b. b > Age In an equation for ‘c’: c = coerce (c :: Int > forall b. b > Int) :: Int > forall b. b > Age In the instance declaration for ‘C Age’  19  c = coerce (c :: Int > forall b. b > Int) :: Int > forall b. b > Age  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Since this does typecheck with the TypeApplications
based approach, I'll go with that one.
comment:30 Changed 7 months ago by
Ah, correction, I can reproduce this. Weird. I'll look.
Gah. Yet another unrelated bug, this time in TcDerivInfer.simplifyDeriv
. Patch coming.
comment:31 Changed 7 months ago by
Blocking:  14883 removed 

Differential Rev(s):  → Phab:D4895 
Status:  new → patch 
Phab:D4895 implements the deriving
related bits.
comment:32 followup: 33 Changed 7 months ago by
OK, this commit fixes the problem reported in comment:22, and adds the code there as a regression test.
This is the third separate bug exposed by the original bug report. Wow.
commit 261dd83cacec71edd551e9c581d05285c9ea3226 Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Mon Jun 25 17:42:57 2018 +0100 Fix TcLevel manipulation in TcDerivInfer.simplifyDeriv The level numbers we were getting simply didn't obey the invariant (ImplicInv) in TcType Note [TcLevel and untouchable type variables] That leads to chaos. Easy to fix. I improved the documentation. I also added an assertion in TcSimplify that checks that level numbers go up by 1 as we dive inside implications, so that we catch the problem at source rather than than through its obscure consequences. That in turn showed up that TcRules was also generating constraints that didn't obey (ImplicInv), so I fixed that too. I have no idea what consequences were lurking behing that bug, but anyway now it's fixed. Hooray.
Are we done now? (Once Ryan has committed the stuff in comment:31.)
comment:33 Changed 7 months ago by
Replying to simonpj:
Are we done now?
I certainly hope so! :) I've rebased Phab:D4895 on top of your most recent changes, so that should wrap things up on this ticket.
Another question remains of what to do with #9123, which requests that GeneralizedNewtypeDeriving
emit quantified constraints involving Coercible
. But this ticket shows that doing so often leads to disaster. In light of this, should we close #9123 as wontfix?
comment:34 Changed 7 months ago by
As comment:63 says (on #9123) I don't think we should ever infer quantified constraints, regardless of this ticket. So I'm fine with closing #9123
comment:35 Changed 7 months ago by
Status:  patch → merge 

comment:36 Changed 7 months ago by
I'm putting this in merge state since there are already a few patches that need to be backported. However, the issue here isn't quite fixed until Phab:D4895 is merged to master
.
comment:38 Changed 7 months ago by
Blocking:  9123 removed 

Test Case:  quantifiedconstraints/T15290, T15290a → quantifiedconstraints/T15290{,a,b}, deriving/should_compile/T15290{c,d}, deriving/should_compile/T14883 
With the commit in comment:37, that should take care of business.
As far as which commits to merge, my understanding is that you would need everything mentioned in this ticket, which encompasses:
 32eb41994f7448caf5fb6b06ed0678d79d029deb
 9fc40c733ba8822a04bd92883801b214dee099ca
 261dd83cacec71edd551e9c581d05285c9ea3226
 132273f34e394bf7e900d0c15e01e91edd711890
Does that sound right?
Also, I apologize in advance to Ben :)
comment:39 Changed 6 months ago by
Resolution:  → fixed 

Status:  merge → closed 
This actually wasn't as bad as I was fearing:
 32eb41994f7448caf5fb6b06ed0678d79d029deb was merged with 61adfbe6f9926daf06031b7da2522f73addf75dc.
 9fc40c733ba8822a04bd92883801b214dee099ca was merged with 7e19610c925c45ade589b573a7e1c247cd8265ef
 261dd83cacec71edd551e9c581d05285c9ea3226 was merged with 145f7c663e6df4ecfa848c0e2e478454cf9fb1d9.
 132273f34e394bf7e900d0c15e01e91edd711890 was merged with c0323d979d3676f919d6d02aecad7a8bfdcb8b8d
Simpler test case: