#8503 closed bug (fixed)

New GeneralizedNewtypeDeriving check still isn't permissive enough

Reported by: goldfire Owned by: goldfire
Priority: normal Milestone:
Component: Compiler Version: 7.7
Keywords: Cc: dimitris@…, sweirich@…, diatchki
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: #8548 Blocking:
Related Tickets: #8541 Differential Revisions:

Description

Roman Cheplyaka writes:

I just tried compiling smallcheck with GHC HEAD, and it didn't work out:

 Test/SmallCheck/SeriesMonad.hs:41:7:
     Can't make a derived instance of ‛MonadLogic (Series m)’
       (even with cunning newtype deriving):
       it is not type-safe to use GeneralizedNewtypeDeriving on this class;
       ‛msplit’, at type ‛forall a.
                          m a -> m (Maybe (a, m a))’, cannot be converted safely
     In the newtype declaration for ‛Series’

So GHC now looks at the methods, but the problem is still there.

I would agree that msplit's type is problematic (due to the nested m's), but Simon and Richard previously said that it should work, so I'm confused.

Change History (41)

comment:1 Changed 21 months ago by goldfire

This is subtler than I thought.

Let's take a simple case:

  class C m where
    meth :: m (m a)

  instance C Maybe where
    meth = Nothing

  newtype NT a = MkNT (Maybe a)
    deriving C

In the derived instance for C NT, we need this:

$meth_C_NT = $meth_C_Maybe |> co
  where
    co :: forall (a :: *). Maybe (Maybe a) ~R# NT (NT a)

What is co? Ideally, it would be

co = forall (a :: *). Sym NTCo:NT[0] (Sym NTCo:NT[0] <a>)

but that doesn't role-check! NTCo:NT[0] has type NT ~R# Maybe. But, to apply that coercion to another requires an AppCo, which in turn requires its second argument to have a nominal role. The underlying problem here is essentially that eta-reducing the newtype coercion loses information about the roles of its parameters. After all, if Maybe's parameter were at a nominal role, then this deriving would be bogus. By eta-reducing, we're forgetting that Maybe's parameter's role is other than nominal.

What to do? One possible solution is to allow AxiomInstCo to be oversaturated, and then role information could be stored in an axiom (indeed, role information for all non-eta-reduced parameters is already there). This isn't a terrible plan, but perhaps it has further ramifications that I'm not currently seeing.

comment:2 Changed 21 months ago by simonpj

  • Cc dimitris@… sweirich@… added

Wait. Suppose we have g1 : m ~R n, and g2 : a ~R b. Then you might think we can conclude that g1 g2 : m a ~R n b. But as you point out, our current rules say not. (I'm looking in docs/core-spec/core-spec.pdf.)

But why do they say not? What does it mean for m to be representationally-equal to n (something that really only makes intuitive sense at kind *), other than "if you apply them to representationally-equal arguments you get representationally-equal types?

Another alternative would be NOT to eta-reduce the newtype coercion. See Note [Newtype eta] in TyCon.lhs. It's much less important than it was because we are no longer coercing dictionaries. But there would still be a cost, as the note points out.

Simon

comment:3 Changed 21 months ago by sweirich

Perhaps another option is to generalize TyConAppCo so that it allows the heads to differ as long as they are (representationally) equal and we have role information for each head. That's slightly more general than changing AxiomInstCo as you'd get transititivity...

comment:4 Changed 21 months ago by simonpj

Stephanie did you think about para 2 of my comment? Why not just change the typing rules?

Simon

comment:5 Changed 21 months ago by sweirich

Simon, there is more to it than just "if you apply them to representationally-equal arguments you get representationally-equal types?" We need to also look at the roles of the parameters in the application.

Consider this example:

type family F a where
   F Moo = Char
   F _      = Int

newtype T a = MkT (F a)   
newtype U a = MkU (T a)

So T and U are representationally equal, but their parameter has nominal role. That means that we can safely conclude

T Moo ~/R U Moo

but it would *not* be safe to say

T Moo ~/R U Int

because then we would have Char ~/R Int.

That is why I was suggesting the change to TyConAppCo. We're not tracking the parameter roles in kinds, so the only place we can look for them is in the head of an application.

comment:6 Changed 21 months ago by simonpj

Good point. Messing with TyConAppCo seems like a sledgehammer to crack a nut, though.

Let's check one thing. Does the problem go away if we say that the axiom for U is

axiom ax7 a : U a ~R T a

that is, if we refrain from eta-reducing the axiom?

If so, I think we can re-visit our reasons for eta-reducing the axiom (see Note [Newtype eta] in TyCon.lhs). I believe the reason was 99% to do with coercing the dictionary in GND. And we aren't doing that any more. Moreover, it seems kind of odd to have representational equality at any kind other than *, doesn't it? Do we have any other source of representational equality at non-* kinds?

Getting rid of the eta reduction would simplify the code a bit, too.

Simon

comment:7 Changed 21 months ago by goldfire

I agree with Stephanie -- the rule Simon was looking at in core-spec (Co_AppCo, p. 10) is that way for a good reason.

Why eta-reduce? Because it allows for more lifting of newtype coercions, via the Coercible mechanism. For example, if we don't eta-reduce

newtype NTMaybe a = MkNT (Maybe a)

then we couldn't derive, say StateT Int NTMaybe a ~R StateT Int Maybe a. So, we don't need eta-reduction as much as maybe we once did, but it's still useful.

One other alternative is to have the cake and eat it too: a newtype declaration like the one for NTMaybe can create two axioms: one eta-reduced and one not. There would have to be some logic to choose which axiom to use, but this would allow for all the constructions that we might want. (Strawman implementation: always use the eta-reduced version, except in GND and in Coercible code where we need the extra role info.)

I'm personally not a big fan of the generalization of TyConAppCo. Stephanie's proposal means that the TyConAppCo would have to store two TyCons and a coercion between them, and all the code that thinks about TyConAppCos would now have to consider the possibility that the two TyCons are different.

But, after all this, I still think I favor my original idea: allow oversaturated AxiomInstCos, and store extra role information in CoAxioms accordingly. Can we think of reasons why this is bad? We already allow oversaturated TyConAppCos (in fact, we require them to be oversaturated, as a TyConAppCo can't be on the left of an AppCo). We would introduce a similar invariant between AxiomInstCo and AppCo.

comment:8 Changed 21 months ago by simonpj

Can you outline the AxiomInstCo idea in a bit more detail? Sounds plausible.

comment:9 follow-up: Changed 21 months ago by goldfire

Hold the phone! There is an easier solution to the original problem!

In my first comment, I wanted a coercion co :: forall (a :: *). Maybe (Maybe a) ~R NT (NT a), and then I proposed a possible value of that type that was ill-roled. But, here is a well-roled value:

co = co1 ; co2

co1 :: forall (a :: *). Maybe (Maybe a) ~R Maybe (NT a)
co1 = forall (a :: *). Maybe (sym NTCo <a>_N)

co2 :: forall (a :: *). Maybe (NT a) ~R NT (NT a)
co2 = forall (a :: *). sym NTCo <NT a>_N

If we convert the pieces one at a time and then use transitivity, we're all OK. I remember battling against this problem over the summer.

So, now we have a new question: how to get GHC to find this solution? Luckily, we happen to have a solver lying around that does just that: the Coercible mechanism. I imagine we could get the GND code to just call the Coercible code for each method. In fact, I considered this approach when improving the GND mechanism a few weeks ago, but thought it was overkill.

My guess is that this would Just Work, when implemented. It might simplify the code a bit, too, but be somewhat less efficient (at compile time) at doing GND. I think this is reasonable.

Taking the idea a bit further, what if the Coercible mechanism can't derive a coercion for a particular method? It would have to produce unsolved Coercible constraints... which we could just add to the constraints on the GND instance! This would allow more GND's to work than we had hoped for, such as this example:

type family F a
class C a where
  meth :: a -> F a

type instance F Int = Bool
class C Int where
  meth = (> 0)

type instance F Age = Bool
newtype Age = MkAge Int
  deriving C      -- just works, no extra constraints because F Age = F Int

type instance F [a] = a
class C [a] where
  meth = head

type instance F (List a) = Int
newtype List a = MkL [a]
  deriving C     -- this would create an instance with head "instance (Coercible a Int) => C (List a) where ..."

This all seems quite reasonable behavior, though we would want to make sure we don't produce constraints like Coercible Int Bool.

Thoughts? Is this a good plan? We could always, as a first pass, implement GND in terms of Coercible and fail if there are any unsolved constraints, working for C Age above but not C (List a).

Last edited 21 months ago by simonpj (previous) (diff)

comment:10 Changed 21 months ago by simonpj

Cool idea. I like it.

For the most part, the 'deriving' mechanism generates an instance decl in HsSyn RdrName and feeds it through the renamer and type checker. We could do that for deriving decls too, like this:

newtype Age = MkAge Int deriving( C )

would generate

instance C Int => C Age where
  meth = coerce (meth :: Int -> F Int)

Here we simply call coerce, which wakes up the Coercible stuff. It's a bit of a nuisance that we have to specify a type signature (in HsType) for meth, so that the from-type of the coerce is known, but not too bad.

What you say about inferring Coercible constraints also makes sense.

This would have another benefit: making GND much more uniform with the other instances. See TcEnv.InstInfo. We can probably get rid of NewTypeDerived altogether, by generating a VanillaInst instead!

Simon

comment:11 Changed 21 months ago by goldfire

Posted this to ghc-devs. Realizing it makes more sense here:

I've run up against a limitation of Coercible I'd like to know more about. Currently, the stage2 compiler on my branch fails to build because of the problem.

In Module.lhs, there is this line:

newtype PackageId = PId FastString deriving( Eq, Typeable )

The deriving mechanism sensibly prefers to use the GND mechanism when it can, and it can (seemingly) for Eq here. But, I get this error:

compiler/basicTypes/Module.lhs:297:46:
   No instance for (ghc-prim:GHC.Types.Coercible FastString PackageId)
     because ‛PackageId’ is a recursive type constuctor

This is curious, because PackageId is manifestly not recursive. A little poking around tells me that any datatype mentioned in a .hs-boot file is considered recursive. There is sense to this, but the error message sure is confusing. In any case, this opens up a broader issue: we want GND to work with recursive newtypes. For example:

class C a where
 meth :: a

instance C (Either a String) where
 meth = Right ""

newtype RecNT = MkRecNT (Either RecNT String)
 deriving C

The above code works just fine in 7.6.3. But, if Coercible isn't allowed over recursive newtypes, then this wouldn't work if GND is implemented in terms of coerce.

So, my question is: why have this restriction? And, if there is a good reason for it, it should probably be documented somewhere. I couldn't find mention of it in the user's guide or in the haddock docs. If we do keep this restriction, what to do about GND? Seems like this may kill the idea of implementing GND in terms of coerce, but that makes me sad.

comment:12 Changed 21 months ago by goldfire

Simon PJ's response:

Ah, life is never as simple as you hope.

The whole treatment of recursive types is a bit flaky in GHC. For newtypes here is the motivation

	newtype R = MkR R

Now if we have an instance

	instance Coercible a R => Coercible a R

we aren't going to make much progress. Mutual recursion is similar.

This is very much a corner case. I think that if the recursion is under a type constructor eg

	newtype R1 = MkR [R1]

then we are fine. But the current test is conservative. I worry about

	newtype R2 a = MkR (F a)

because perhaps

	type instance F Int = R2 Int

and now R2 Int is just like R. But GHC won't spot this today.

In any case, I suppose that, provided it was documented, GND could simply ignore the recursion problem, behave as advertised, and if that gives a loop it's the programmer's fault.

Things in hs-boot files are treated (again conservatively) as if they might be recursive.

A related thing is unpacking data types. Consider

	data T = MkT {-# UNPACK #-} !S
	data S = MkS {-# UNPAXCK #-} !Int {-# UNPAXCK #-} !Int

A S-value is represented as a pair of Int# values. And similarly T. But what about

	data S2 = MkS2 {-# UNPACK #-} !Int {-# UNPACK #-} !S2

We don’t want to unpack infinitely. Strictness analysis also risks infinitely unpacking a strict argument.

I think the rules for newtypes could be different (and perhaps more generous) than for data types.

comment:13 Changed 21 months ago by goldfire

Yuck.

I'm leery of creating a way for the type-checker to loop without turning on UndecidableInstances. And, with the R2 example that Simon gives, the newtype and the relevant type family instance might be in different modules, so detecting even so simple an infinite regress may be problematic. (And, note that the pieces on their own are innocent-looking.)

I've also just looked at Note [Recursive newtypes] in TcDeriv. This note explains why GND works for recursive newtypes. I repeat it here:

Note [Recursive newtypes]
~~~~~~~~~~~~~~~~~~~~~~~~~
Newtype deriving works fine, even if the newtype is recursive.
e.g.    newtype S1 = S1 [T1 ()]
        newtype T1 a = T1 (StateT S1 IO a ) deriving( Monad )
Remember, too, that type families are curretly (conservatively) given
a recursive flag, so this also allows newtype deriving to work
for type famillies.

We used to exclude recursive types, because we had a rather simple
minded way of generating the instance decl:
   newtype A = MkA [A]
   instance Eq [A] => Eq A      -- Makes typechecker loop!
But now we require a simple context, so it's ok.

I'm confused by the last line. In the code above the note, a context is generated that includes, for this example, Eq [A]! Where does the loop get broken?

Regardless, here's a possible solution: if Coercible over recursive newtypes is sound but otherwise in danger of causing a loop, we could just require UndecidableInstances to get the Coercible mechanism to go down this road. In this scenario, my example (with RecNT) would fail to use GND without UndecidableInstances but should succeed with it. We can even give a helpful error message in this scenario.

Or, perhaps even better: could the Coercible mechanism use TyCon.checkRecTc? That function seems to be designed for exactly this scenario, which is where we need to do newtype expansion but don't want to fall into a black hole. That might complicate the Coercible code, but I think it would be a step in the right direction. We could still allow users to specify UndecidableInstances to bypass even this check... but my guess is that checkRecTc would work exactly in the correct cases, meaning that bypassing the check is sure to cause the type-checker to loop. Other, more informed opinions are very welcome here.

Lastly, is there a solid reason to require that the recursiveness of a type in a hs-boot file and the recursiveness of the real type are the same? It looks to me that it would be sound to assume types in hs-boot files are recursive, but then not to inherit this trait when processing the real thing. That would fix the problem with compiling Module.lhs, and it would save some embarrassment if we were to suggest UndecidableInstances to compile a very ordinary-looking newtype!

comment:14 Changed 21 months ago by nomeata

I was conservative when disallowing recursive newtypes for Coercible, but quite possibly too conservative. I also wanted to keep the code simple (Note that it just keeps generating constraints and passing them back to the constraint solver; it does *not* build the whole coercion in one go).

I wasn’t aware of TyCon.checkRecTc and I’ll look into it. Thanks for pointing that out.

comment:15 Changed 21 months ago by nomeata

Using just TyCon.checkRecTc is too permissive for Coercible. checkRecTc succeeds for Fix (Either x) (where newtype Fix f = MkFix (f (Fix f))) for all type x. But then we’d generate the instances

instance Coercible (Either x (Fix (Either x))) b => Coercible (Fix (Either x)) b
instance Coercible a (Either x (Fix (Either x))) => Coercible a (Fix (Either x))

so trying to solve the constraint Coercible (Fix (Either Age)) (Fix (Either Int)) will loop. (With the current implementation, which hooks into the general constraint resolving, I’d expect it to not loop at compile time, but create a diverging witness, and crash at run time. Neither of these are desired).

Now what about your example, newtype RecNT = MkRecNT (Either RecNT String). Assume that Coercible would work for it, and assume there is also newtype RecNT2 = MkRecNT2 (Either RecNT2 String). Then, similarly, solving Coercible RecNT RecNT2 will loop with the current implementation...

So it is not a matter of relaxing the checks; if we want to support recursive newtypes in Coercible, the algorithm needs to be generally overhauled.

comment:16 Changed 21 months ago by goldfire

Yes, I agree, sadly.

Simon PJ and I (in a phone call) thought that we could solve all our problems with topNormaliseType_maybe, which "evaluates" out any newtypes and type functions that appear at the top of a type. If there is no way to reduce a type at the top level, the function fails. Because the Coercible code really only examines the top level, we thought this was sufficient. However, it's not, because of the example you (nomeata) give, with RecNT and RecNT2.

My only thought now for how to do this is to record in the wanted constraint which newtypes have been expanded, perhaps using the checkRecTc technology. This would mean either creating a new constructor for Ct or a new field somewhere. Perhaps creating a new constructor isn't so bad -- that's how nominal equality is handled. Canonicalisation can then convert a normal class-based constraint into the new CCoercible or something. I still think there is hope here, and I do think we should strive to include recursive newtypes in this approach.

In my attempt to fix this all, I've done some refactoring in getCoercibleInst. You can see my work at my github repo, branch coerce. That branch also introduces a GenCoercion class containing Coercion and TcCoercion. That may or may not be a good idea, but it worked nicely with topNormaliseType_maybe, which has to sometimes produce a Coercion and sometimes a TcCoercion.

I've also discovered that Coercible really ought to be poly-kinded. If we have newtype List a = MkList [a], then we might want Coercible (StateT Int [] a) (StateT Int List a), which would lead to Coercible [] List, but that's ill-kinded! I think the first coercion is quite legitimate, and so we should find some way of allowing it. Generalizing Coercible seems to be the obvious way forward, but other possibilities are out there, I suppose.

This problem (with Coercible being mono-kinded) came up in practice as a core-lint failure when compiling the libraries in my branch.

comment:17 Changed 21 months ago by simonpj

  • Cc diatchki added

Let's note that even with Fix there is a legitimate and useful coercion Coercible (Fix (Either x)) (Either x (Fix (Either x))). We can write it by hand, and you might want to get from the Fix form to the Either form. So the same instance declaration may terminate when solving some constraints, but not for others.

The constraint solver already stores a "depth" in each constraint. The depth is incremented by 1 each time you use an instance declaration. For example, when you use instance Eq a => Eq [a] to solve d1:Eq [Int], by reducing it to d2:Eq Int, then d2 has a depth one greater than d1. Since such instance declarations remove a type constructor, a deep recursion implies a deeply nested type, like [[[[[[Int]]]]]. So (proposal) maybe we can simply depth-bound the solver. In fact it already is; this is the -fcontext-stack flag.

(Actually, in fact I fear that we may instead construct a recursive dictionary instead, which we probably do not want for newtypes, though we do for data types, because we'll see a constraint we have already solved. See Scrap your boilerplate with class for why we want recursive dictionaries.)

Here is one other idea. Suppose we have the wanted constraint Coercible [alpha] [Int]. Should we use the Coercible a b => Coercible [a] [b] instance to solve it? Well, if it turns out that alpha (a unification variable) ultimately is Int, then doing so would not be wrong, but it would be a waste because the identity coercion will do the job. So maybe this is a bit like the Equal type family in the Closed type families paper: we should not do the list/list reduction unless the argument types are "apart" (in the terminology of the paper).

But that would be too strong. Consider

f :: Coercible a b => [a] -> [b]
f x = coerce x

This should work, but it requires use of that list/list instance, and we don't know that a and b are un-equal. It's just that in this context we can treat a and b as skolems and hence "apart" for this purpose. Except, even then it's not quite right: we could have

f :: (a~b, Coercible a b) => [a] -> [b]

and now a and b are provably equal. (Or some GADT version thereof.) So I think we probably need the depth-bound thing too.

Do any of these ideas make sense to you guys? I'll add Iavor to the cc list.

comment:18 Changed 21 months ago by nomeata

(Actually, in fact I fear that we may instead construct a recursive dictionary instead, which we probably do not want for newtypes, though we do for data types, because we'll see a constraint we have already solved. See ​Scrap your boilerplate with class for why we want recursive dictionaries.)

JFTR: Last time I checked, we did, leading to a non-terminating Coercion value.

comment:19 Changed 21 months ago by simonpj

I discussed with Joachim. The "apartness" idea definitely doesn't work. Consider

newtype Fix1 x = F1 (x (Fix1 x))
newtype Fix2 x = F2 (x (Fix2 x))

and try solving Coercible (Fix1 (Either Age)) (Fix2 (Either Int)). Everything is fully known, and always apart, yet we get a loop.

Moreover, analysing the definitions to find loop breakers (as GHC does now) fails in the presence of type functions

newtype Bad a = B (F a)
type instance F Int = Bad Int

Conclusion: the depth-bound idea is the only real option.

We also need to prevent the construction of recursive dictionaries, but we can use the depth of a constraint to stop that too; do not solve a constraint of depth n by using a constraint of lower depth. This is rather conservative, but it's enough to prevent recursive dictionary construction.

comment:20 Changed 21 months ago by nomeata

See #8541 for a ticket discussing poly-kind Coercible.

comment:21 Changed 21 months ago by goldfire

Yes, the depth-bound seems sensible and is probably the only real solution to this problem.

We should be aware of a particularly nasty case, like this:

Coercible (Maybe (Fix Maybe)) (Fix Maybe)

This should be solvable (and I posit that more sensible cases might come up in practice). The current algorithm simplifies the left-hand type (LHT) as far as it can, then simplifies the right-hand type (RHT) as far as it can. I would worry that the depth would hit its maximum when reducing the LHT and then refuse to simplify the RHT. Even if we tracked depths separately for the two sides, the right side would hit the maximum depth right before the two sides unify, leading to failure, no matter what the depth is!

Note that if we just switch the order of the arguments to Coercible, this goal is easy to solve, after one reduction on the LHT. Having the solubility of a symmetric constraint depend on the order of arguments is undesirable.

I have no good ideas of how to fix this, at the moment.

comment:22 Changed 21 months ago by nomeata

Have you checked that it fails? I believe it would work:

Coercible (Maybe (Fix Maybe)) (Fix Maybe)

is only matched by

instance Coercible a (Maybe (Fix Maybe) => Coercible a (Fix Maybe)

so we are left with

Coercible (Maybe (Fix Maybe)) (Maybe (Fix Maybe))

which is solved by the reflexive instance

Coercible a a

(I’m not claiming that all cases work as smoothly, but they need to be a bit more constructed :-))

comment:24 Changed 21 months ago by simonpj

For the recurisve-newtype problem (ie the main topic of this ticket, now that we have moved polykinded Coercible to #8541), the approach (developed by Joachim and me) is to

A) Add a feature to the constraint solver to prevent recursive dictionaries for specially marked instances (for now only used for Coercible). Rationale: Such dictionaries (which are fine for most classes like Show) would make coerce diverge. Implementation: Use the depth counter and do not use lower depths to solver constraints with a higher depth. This is of course a very conservative approximation, but should be sufficient.

B) Use the regular constraint depth bound to prevent looping at compile time. In order for that to be more useful, count constraint solving and type function resolving separately.

comment:25 Changed 21 months ago by nomeata

ignore this; ticket race condition noise

Last edited 21 months ago by nomeata (previous) (diff)

comment:26 Changed 21 months ago by nomeata

As a first step, I implemented separate depth counters for regular constraints and type function application.

User-visible changes: Flag -ftype-function-stack, in addition to -fcontext-stack. Feel free to bikeshed you think the name is inappropriate. The defaults for these values are discussed in #5395 (current 200 resp. 20).

See http://git.haskell.org/ghc.git/shortlog/refs/heads/wip/T8503 for my work in progress, and http://git.haskell.org/testsuite.git/shortlog/refs/heads/wip/T8503 for the corresponding test suite updates.

comment:27 Changed 21 months ago by nomeata

I have something that is roughly working, enough to notice problems. While it successfully prevents Coercible Fix (Either Int) from looping or generating recursive dictionaries, it does not help a lot against

newtype Void a = Void (Void (a,a))

foo5 = coerce :: Void () -> ()

Even with a depth of 20, this filly up my memory quickly, especially trying to print the final constraint.

Do we have to live with the fact that there will likely always be ways to make the compiler use too many resources? Or should coercing recursive newtypes require UndecidableInstances to be enabled?

comment:28 Changed 21 months ago by simonpj

There are plenty of other ways to construct exponentially-sized types (even in H-M),so I don't think we should worry here. Remember too that type functions mean that the entire notion of a "recursive newtype" is suspect.

comment:29 Changed 21 months ago by nomeata

Got that code in a working form. I don’t claim to know the solver well enough to be completely certain that there is not a way left to create a recursive dictionary, but at least the examples that I tried worked. Commits 6f5c183cb798a5d5e1011417f1f211834e4e9215 (GHC) and ec83ce7530af5474a3ad49d7120913c7f22266f0 (testsuite); for convenience, here is the note describing the design:

Note [Preventing recursive dictionaries]

We have some classes where it is not very useful to build recursive
dictionaries (Coercible, at the moment). So we need the constraint solver to
prevent that. We conservativey ensure this property using the subgoal depth of
the constraints: When solving a Coercible constraint at depth d, we do not
consider evicence from a depth <= d as suitable.

Therefore we need to record the minimum depth allowed to solve a CtWanted. This
is done in the SubGoalDepth field of CtWanted. Most code now uses mkCtWanted,
which initializes it to initialSubGoalDepth (i.e. 0); but when requesting a
Coercible instance (requestCoercible in TcInteract), we bump the current depth
by one and use that.

There are two spots where wanted contraints attempted to be solved using
existing constraints; doTopReactDict in TcInteract (in the general solver) and
newWantedEvVarNonrec (only used by requestCoercible) in TcSMonad. Both use
ctEvCheckDepth to make the check. That function ensures that a Given constraint
can always be used to solve a goal (i.e. they are at depth infinity, for our
purposes)

comment:30 Changed 21 months ago by nomeata

I cherry-picked Richard’s implementation of GND via coerce (c76fed) onto wip/T8503 and GHC compiles (after make clean) just fine – which is great.

There are test suite failures, though A lot are performance degrations (some, if they are about the performance of GHC, are to be expected, the Coercible machinery with subsequent simplification is not the fastest code). The others are:

Unexpected failures:
   codeGen/should_run            cgrun068 [exit code non-0] (normal)
   deriving/should_compile       T2856 [exit code non-0] (normal)
   deriving/should_compile       drv015 [exit code non-0] (normal)
   deriving/should_fail          T1496 [stderr mismatch] (normal)
   deriving/should_fail          T2721 [stderr mismatch] (normal)
   deriving/should_fail          T4846 [stderr mismatch] (normal)
   deriving/should_fail          T7148 [stderr mismatch] (normal)
   deriving/should_fail          T7148a [stderr mismatch] (normal)
   deriving/should_run           drvrun019 [exit code non-0] (normal)
   gadt                          CasePrune [stderr mismatch] (normal)
   gadt                          gadt6 [exit code non-0] (normal)
   ghci.debugger/scripts         print018 [bad stdout] (ghci)
   indexed-types/should_compile  DerivingNewType [exit code non-0] (normal)
   indexed-types/should_compile  IndTypesPerf [bad exit code] (normal)
   indexed-types/should_compile  T2850 [exit code non-0] (normal)
   indexed-types/should_compile  T3423 [exit code non-0] (normal)
   indexed-types/should_compile  T4185 [exit code non-0] (normal)
   indexed-types/should_compile  T5955 [bad exit code] (normal)
   indexed-types/should_compile  T7474 [exit code non-0] (normal)
   lib/integer                   integerConstantFolding [bad stderr] (normal)
   polykinds                     T7332 [exit code non-0] (normal)
   roles/should_fail             Roles10 [stderr mismatch] (normal)
   simplCore/should_compile      T4203 [exit code non-0] (normal)
   typecheck/should_compile      T3955 [exit code non-0] (normal)
   typecheck/should_fail         T5246 [stderr mismatch] (normal)

Of these, there are a few where we get unresolved Coercible instances due to roles (and many of them might be genuine and can probably be marked as expected to fail), but there is also a number of panic and failed assertions.

wip/T8503 itself validates, so these were either introduced or triggered by implementing GND via coerce. Probably triggered, given that the GND code now generates mostly straight-forward code.

I’ll start looking into some of them tomorrow, but Richard, if you feel like helping debugging them, that would be appreciated. Some of them appear in code that I do know know much about, such as module interfaces.

comment:31 Changed 21 months ago by nomeata

  • Blocked By 8548 added

comment:32 Changed 21 months ago by nomeata

Is it hijacking this ticket to discuss the impact of GND-via-coerce here?

Anyways, feature request #2850 will be broken if we do GND-via-coerce. Four tickets are broken because of #8548 (Coercible not working for newtype instance yet), these will be fixable.

The remaining ones (TEST="print018 cgrun068 T4203 drvrun019 T3955 T7474 T3423 IndTypesPerf T5246 integerConstantFolding gadt6 T7332 drv015") cause panics, looking into them now.

comment:33 Changed 21 months ago by goldfire

I think the issue with #2850 is fixable. See that ticket.

I actually think these knock-on effects of the GND-via-coerce decision are good. They're forcing us to get Coercible right!

comment:34 Changed 21 months ago by nomeata

Yes, it is a horribly effective testsuite ;-)

comment:35 in reply to: ↑ 9 Changed 21 months ago by nomeata

Replying to goldfire:

Hold the phone! There is an easier solution to the original problem!

\[..\]

Thoughts? Is this a good plan? We could always, as a first pass, implement GND in terms of Coercible and fail if there are any unsolved constraints, working for C Age above but not C (List a).

I’ve been trying to get your attempt to work. It works for a lot of easy cases, and it works in theory, but there is an implementational difficulty with extra type variables in the instance. Consider:

import GHC.Exts
class Cls a where meth :: a
newtype Id m = Id m deriving Cls

The instance we want to generate is

instance forall m. Cls m => Cls (Id m) where
    meth = coerce (meth :: m) :: Id m

But that will require ScopedTypeVariables. Question one: Can I generate code at TcGenDeriv stage that uses scoped type variables, without requiring that extension to be enabled in the whole module?

Next problem: Currently the code produces

==================== Derived instances ====================
Derived instances:
  instance T3423.Cls m_ayI => T3423.Cls (T3423.Id m_ayI) where
    T3423.meth
      = GHC.Prim.coerce (T3423.meth :: m_ayI) :: T3423.Id m_ayI

so there is no forall in the instance head. For newtype ... deriving Cls it might be possible to add that (although I did not yet find where), but the user should be able to specify

deriving instance Cls m => Cls (Id m)

without having to add forall m.. I’m not sure what to do here.

It would be best if we could generate code that works without having to specify types in the method definition at all, maybe using something like $ClsId = case $superClassDict of D:Cls meth => D:Cls (coerce meth), but I do not see how $superClassDict should look like.

comment:36 Changed 21 months ago by nomeata

My analysis in the previous comment was wrong; SPJ found out that the problem seems to lie in the calculation of defined and used variables for derived instances. Debugging...

comment:37 Changed 21 months ago by nomeata

Ok, the problem were two missing characters:

@@ -432,7 +432,7 @@ renameDeriv is_boot inst_infos bagBinds
         =       -- Bring the right type variables into
                 -- scope (yuk), and rename the method binds
            ASSERT( null sigs )
-           bindLocalNames (map Var.varName tyvars) $
+           bindLocalNamesFV (map Var.varName tyvars) $
            do { (rn_binds, fvs) <- rnMethodBinds (is_cls_nm inst) (\_ -> []) binds
               ; let binds' = InstBindings { ib_binds = rn_binds
                                            , ib_pragmas = []

but now everything seems to work.

I’m running validate right now. If it goes through, any objections to pushing wip/T8503 to master and closing this bug?

comment:38 Changed 21 months ago by goldfire

Please push when ready.

And, re ScopedTypeVariables, you're right -- we do need that extension. But, see here -- the extension is enabled just over the code that needs it.

Thanks for taking the last leg on this one!

comment:39 Changed 21 months ago by Joachim Breitner <mail@…>

In 6468beebcf2b3a2dd9cbedd7b6dc9c7adaee626b/testsuite:

Add test cases for Coercing recursive newtypes (#8503)

comment:40 Changed 21 months ago by Joachim Breitner <mail@…>

In 94128d393c820ed82f61052414cc1ffde8b2af82/testsuite:

Updates perf numbers after #8503 implementation

comment:41 Changed 21 months ago by nomeata

Ok, pushed. Closing this ticket (is is far too long anyways, and trac spends too much time generating it), so any new issues with Coercible or GND please in new tickets.

comment:42 Changed 21 months ago by nomeata

  • Resolution set to fixed
  • Status changed from new to closed

It seems that trac does not do NLP, but Richard does. So again: Closing the ticket...

Note: See TracTickets for help on using tickets.