#9117: Coercible constraint solver misses one
------------------------------------+-------------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.8.2
Keywords: | Operating System: Unknown/Multiple
Architecture: Unknown/Multiple | Type of failure: None/Unknown
Difficulty: Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: |
------------------------------------+-------------------------------------
When I say
{{{
import Data.Type.Coercion
import Data.Coerce
eta :: Coercible f g => Coercion (f a) (g a)
eta = Coercion
}}}
I get
{{{
Could not coerce from ‘f a’ to ‘g a’
because ‘f a’ and ‘g a’ are different types.
arising from a use of ‘Coercion’
from the context (Coercible f g)
bound by the type signature for
eta :: Coercible f g => Coercion (f a) (g a)
at /Users/rae/temp/Roles.hs:6:8-44
In the expression: Coercion
In an equation for ‘eta’: eta = Coercion
}}}
But, this coercion is easily expressible in Core. If `(co :: f ~R# g)`
then `(co <a> :: f a ~R# g a)`, where `<a>` is the notation for a
reflexivity coercion for the type `a`. The constraint solver should be
able to do this.
--
Ticket URL: