New GeneralizedNewtypeDeriving check still isn't permissive enough

changed weight to 5

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.

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

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...

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

Simon

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.

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

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.

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

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).

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

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.

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.

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!

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.

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.

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.

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.

(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.

Trac field	Value
Version	7.7
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

New GeneralizedNewtypeDeriving check still isn't permissive enough

Child items ...

Activity

New GeneralizedNewtypeDeriving check still isn't permissive enough

Relates to

Activity