Bug in Coerciible
Richard and I uncovered this
{-# LANGUAGE RoleAnnotations #-}
module Bar( N ) where -- Data constructor not exported
type role N representational
newtype N a = MkN Int
and
{-# LANGUAGE FlexibleContexts #-}
module Foo where
import Data.Coerce
import Data.Type.Coercion
import Bar
f :: Coercible (N a) (N b) => Coercion a b
f = Coercion
This compiles but it should not! It wrongly compiles by using nth (N a ~R N b)
; but (as Fig 4 of the Corcible paper says), we can't decompose a newtype at representational role.
Easy to fix.
Trac metadata
Trac field | Value |
---|---|
Version | 7.10.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | highest |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |