Surprising failure combining QuantifiedConstraints with Coercible
I don't understand what's going wrong here.
-- Fishy.hs
{-# language RankNTypes, QuantifiedConstraints, RoleAnnotations #-}
module Fishy (Yeah, yeahCoercible) where
import Data.Coerce
data Yeah_ a = Yeah_ Int
newtype Yeah a = Yeah (Yeah_ a)
type role Yeah representational
yeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) -> r
yeahCoercible r = r
-- Fishy2.hs
module Fishy2 where
import Fishy
import Data.Type.Coercion
import Data.Coerce
yeah :: Coercion [Yeah a] [Yeah b]
yeah = yeahCoercible Coercion
I get
Fishy2.hs:8:22: error:
• Couldn't match representation of type ‘a’ with that of ‘b’
arising from a use of ‘Coercion’
‘a’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:1-34
‘b’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:1-34
• In the first argument of ‘yeahCoercible’, namely ‘Coercion’
In the expression: yeahCoercible Coercion
In an equation for ‘yeah’: yeah = yeahCoercible Coercion
• Relevant bindings include
yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)
|
8 | yeah = yeahCoercible Coercion
|
Trac metadata
Trac field | Value |
---|---|
Version | 8.5 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |