Opened 15 months ago

Closed 7 months ago

#8984 closed feature request (fixed)

Improve output of failed GeneralizedNewtypeDeriving coercion due to type roles

Reported by: haasn Owned by: goldfire
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: deriving/should_fail/T8984
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description (last modified by simonpj)

When trying to build acme-schoenfinkel (as an example), I came across an error like this:

Control/Category/Schoenfinkel.hs:66:48:
    Could not coerce from ‘cat (cat b c,
                                b) c’ to ‘cat (WrappedSchoenfinkel cat b c, b) c’
      because ‘cat (cat b c, b) c’ and ‘cat (WrappedSchoenfinkel cat b c,
                                             b) c’ are different types.
      arising from the coercion of the method ‘app’ from type
                   ‘forall b c. cat (cat b c, b) c’ to type
                   ‘forall b c.
                    WrappedSchoenfinkel cat (WrappedSchoenfinkel cat b c, b) c’
    Possible fix:
      use a standalone 'deriving instance' declaration,
        so you can specify the instance context yourself
    When deriving the instance for (ArrowApply
                                      (WrappedSchoenfinkel cat))

It was not immediately clear to me as a user that this was caused due to it wanting GNT which was now being blocked by type roles (rightfully so, as this instance allows UnsafeCoerce!), and beyond that, what the specific rule that triggered this was.

In this case the failure is due to WrappedSchoenfinkel cat b c not being nominally equal to cat b c, in the type (WrappedSchoenfinkel cat b c, b), which is required to be nominally equal to (cat b c, b) because it's used as a parameter to the variable cat.

Printing a location breakdown and context information similar to this to the user would help understanding and debugging roles a lot.

Change History (12)

comment:1 Changed 15 months ago by haasn

More specifically, the exact type that causes a problem is WrappedSchoenfinkel cat and cat not being nominally equal.

Last edited 15 months ago by haasn (previous) (diff)

comment:2 Changed 15 months ago by simonpj

  • Description modified (diff)

comment:3 Changed 15 months ago by simonpj

  • Description modified (diff)

comment:4 Changed 15 months ago by simonpj

Here's a small test case

{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving #-}
module T8984 where

class C a where
    app :: a (a Int)

newtype N cat a b = MkN (cat a b)  deriving( C )
-- The newtype coercion is   N cat ~R cat

We try to prove Coercible (cat (cat Int) (N cat (N cat Int)). We simplify this (by newtype unrwrapping) to Coercible (cat (cat Int)) (cat (N cat Int)); and now we are stuck.

T8984.hs:7:46:
    Could not coerce from ‘cat a (cat a Int)’ to ‘cat a (N cat a Int)’
      because ‘cat a (cat a Int)’
          and ‘cat a (N cat a Int)’
          are different types.
      arising from the coercion of the method ‘app’
                   from type ‘cat a (cat a Int)’
                     to type ‘N cat a (N cat a Int)’

An alternative strategy would be to see that the newtype axiom is over-applied, and instead decompose the application thus:

Coercible (cat (cat Int) (N cat (N cat Int))
==> (decompose application into two parts)
Coercible cat (N cat),  cat Int ~ N Cat int

Now the first constraint is soluble, but the second would say something like "cannot deduce cat Int ~ N Cat Int.

Joachim, Richard, thoughts?

comment:5 Changed 7 months ago by goldfire

With my update to the solver (preview available at http://github.com/goldfirere/ghc, wip/rae-new-coercible branch), the new error message is thus:

T8984.hs:7:46:
    Couldn't match representation of type ‘cat a (N cat a Int)’
                             with that of ‘cat a (cat a Int)’
    arising from the coercion of the method ‘app’
      from type ‘cat a (cat a Int)’ to type ‘N cat a (N cat a Int)’
    Relevant role signatures:
      type role N representational nominal nominal
    NB: We cannot know what roles the parameters to ‘cat a’ have;
      we must assume that the role is nominal
    When deriving the instance for (C (N cat a))

I like it, and will close this ticket when I merge.

comment:6 Changed 7 months ago by goldfire

Refactoring in my branch has added a small wrinkle here: my version currently accepts the original code.

Let's be concrete:

{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving #-}
module T8984 where

class C a where
    app :: a (a Int)

newtype N cat a b = MkN (cat a b)  deriving( C )

yields an instance

instance (Coercible (cat a (N cat a Int)) (cat a (cat a Int)), C (cat a)) => C (N cat a)

This is actually perfectly sound: GHC is just choosing to abstract over the unprovable Coercible constraint. What do we think of this behavior? Is it desired or not? This seems to be a free choice here: I don't think either option or the other would affect much else.

Implementation note: This is a direct consequence of changes to TcValidity.validDerivPred. Previously (that is, in today's HEAD), a Coercible constraint looked like a class constraint, meaning it was checked to make sure that it wasn't too exotic. In my branch, (wip/rae-new-coercible) Coercible constraints are like equalities, which are allowed unchecked. Thus, the rather exotic constraint above is allowed.

This has all gotten me thinking: Why do we blithely allow equality constraints to be in a derived-inferred context? This ability was added in response to #6088, where the user wanted to use GND to derive an instance based on another instance with an explicit equality in the context. Here is the example from #6088:

class C a

newtype A n = A Int

type family Pos n
data True

instance (Pos n ~ True) => C (A n)


newtype B n = B (A n)
   deriving (C)

This is now accepted.

However, here is a very similar case:

class C1 a b
class C2 a

instance C1 a a => C2 (Maybe a)

newtype N a = MkN (Maybe a)
  deriving C2

This second case is rejected. And yet, they're similar in that the exotic context that might be inferred is specified by the user. It seems a little odd to accept one and reject the other.

So, I propose the following behavior:

  • Reject equality constraints to be inferred for deriving.
  • If deriving failed solely because of checks in validDerivPred, provide the full inferred context in the error message to make it easy for users to work around this restriction.

This would, essentially, break the fix for #6088, and would thus be a regression, because 7.8 incorporates the #6088 fix. But, with the enhanced error message, the breakage would be easy to fix. What do folks think?

comment:7 Changed 7 months ago by simonpj

Yes, I agree with your proposal. We should not blithely accept random (and perhaps unsatisfiable) equality constraints in deriving contexts. You can always specify the context with standalone-deriving if you want.

Weill you execute on this?

Simon

comment:8 Changed 7 months ago by Richard Eisenberg <eir@…>

In 0cc47eb90805f3e166ac4d3991e66d3346ca05e7/ghc:

Rewrite `Coercible` solver

Summary:
This is a rewrite of the algorithm to solve for Coercible "instances".

A preliminary form of these ideas is at
https://ghc.haskell.org/trac/ghc/wiki/Design/NewCoercibleSolver

The basic idea here is that the `EqPred` constructor of `PredTree`
now is parameterised by a new type `EqRel` (where
`data EqRel = NomEq | ReprEq`). Thus, every equality constraint can
now talk about nominal equality (the usual case) or representational
equality (the `Coercible` case).

This is a change from the previous
behavior where `Coercible` was just considered a regular class with
a special case in `matchClassInst`.

Because of this change, representational equalities are now
canonicalized just like nominal ones, allowing more equalities
to be solved -- in particular, the case at the top of #9117.

A knock-on effect is that the flattener must be aware of the
choice of equality relation, because the inert set now stores
both representational inert equalities alongside the nominal
inert equalities. Of course, we can use representational equalities
to rewrite only within another representational equality --
thus the parameterization of the flattener.

A nice side effect of this change is that I've introduced a new
type `CtFlavour`, which tracks G vs. W vs. D, removing some ugliness
in the flattener.

This commit includes some refactoring as discussed on D546.
It also removes the ability of Deriveds to rewrite Deriveds.

This fixes bugs #9117 and #8984.

Reviewers: simonpj, austin, nomeata

Subscribers: carter, thomie

Differential Revision: https://phabricator.haskell.org/D546

GHC Trac Issues: #9117, #8984

comment:9 Changed 7 months ago by goldfire

The patch above does not implement the proposal in comment:6 and agreed to in comment:7. I'll implement this proposal soon, but it will likely miss the 7.10 branch. This is OK -- it won't hurt anyone to have this unfixed.

comment:10 Changed 7 months ago by goldfire

  • Owner set to goldfire
  • Test Case set to deriving/should_fail/T8984

comment:11 Changed 7 months ago by Richard Eisenberg <eir@…>

In 02b4845e07ef7110b2f735f323eb8748903330ff/ghc:

Consider equality contexts exotic, uninferrable by "deriving"

See comments in #8984. This takes back the fix for #6088.

comment:12 Changed 7 months ago by goldfire

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

All done now.

Note: See TracTickets for help on using tickets.