[GHC] #10715: Possible regression in Coercible a (X a) between 7.8 and 7.10

[GHC]

#10715: Possible regression in Coercible a (X a) between 7.8 and 7.10
-------------------------------------+-------------------------------------
        Reporter:  inaki             |                   Owner:
            Type:  bug               |                  Status:  new
        Priority:  normal            |               Milestone:
       Component:  Compiler          |                 Version:  7.10.1
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |               Test Case:
      Blocked By:                    |                Blocking:
 Related Tickets:                    |  Differential Revisions:
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Interesting.  HEAD reports
 {{{
 T10715.hs:8:13: error:
     Could not deduce: Coercible a (X a)
     from the context: Coercible a (X a)
 }}}
 which is even more confusing!

 Here's what is happening

  * GHC treats `Coercible a ty` as a representational equality constraint
 `a ~R ty`.

  * Given an equlity `a ~R ty`, it tries to rewrites other constraints
 mentioning `a`, by replacing `a` with `ty`.

  * But here it can't do that, because `ty` mentions `a`, so we could
 rewrite forever; a kind of occurs-check problem.  And indeed, if we had
 something like
 {{{
 f :: (a ~ [a]) => blah
 }}}
  we really wouldn't expect much to happen because the constraint can't
 possibly be satisfied.

  * However, if the given equality is `a ~R X b`, we CAN use it to rewrite
 the wanted constraint, to get `X b ~R X a`.  And that is soluble by
 decomposition because `X`'s first argument is phantom.  Hence your
 "Surprisingly to me" discovery.

  * If you write a type signature like
 {{{
 f :: (a ~ [a]) => blah
 }}}
  you get an error like
 {{{
 T10715.hs:15:8: error:
     Couldn't match type ‘a’ with ‘[a]’
     ‘a’ is a rigid type variable bound by
         the type signature for: foo :: (a ~ [a]) => a -> [a] -> Bool
         at T10715.hs:15:8
     Inaccessible code in
       the type signature for: foo :: (a ~ [a]) => a -> [a] -> Bool
 }}}
  Maybe we should do the same for `Coercible`?  That would at least give a
 better error message than "can't deduce A from A"!

  * It wouldn't help your use-case.  But do you have to use `Y` in this
 strange recursive way. Why not do this?
 {{{
 newtype FY = FY (ForeignPtr Y)
 data Y
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10715#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler