Skip to content

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information