Possible excessive leniency in interaction between coerce and data families?
Per goldfire's request at #8177, I am promoting this issue into it's own ticket. I am entirely not confident that it represents a bug; I raise the issue because, while it happens to do exactly what I want, I cannot understand *why* it does what I want, and it seems like it might possibly also do related undesirable things.
I have the following situation, which I have distilled from a real use case, retaining its identifiers but eliding a whole bunch of irrelevant detail. The real thing is on GitHub if it helps anyone to see why I want to do this, but it's really a side issue AFAICT.
It's split into two modules, because goldfire had suggested that it might have arisen because the newtype constructor Quantity'
was in scope at the site of the coerce
, this test shows that it arises even when Quantity'
is not in scope.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
module Test
(
Quantity, Unit,
Dimension(..),
Variant(..),
Mass,
KnownVariant(Dimensional)
)
where
data Variant = DQuantity | DUnit
data Dimension = DMass | DLength | DTime -- ... this isn't the real way, it's simplified
data UnitName = UnitName String
class KnownVariant (var :: Variant) where
data Dimensional var :: Dimension -> * -> *
instance KnownVariant DQuantity where
newtype Dimensional DQuantity d v = Quantity' v
instance KnownVariant DUnit where
data Dimensional DUnit d v = Unit' UnitName v
instance (Show v) => Show (Dimensional DQuantity d v) where
show (Quantity' x) = "As A Quantity " ++ show x
type Quantity = Dimensional DQuantity
type Unit = Dimensional DUnit
type Mass v = Quantity DMass v
And the main module:
module Main where
import Test
import Data.Coerce
main = do
let x = 3.7 :: Double
putStrLn . show $ x
let y = (coerce x) :: Mass Double
putStrLn . show $ y
let z = (coerce y) :: Double
putStrLn . show $ z
My question is in two parts:
-
Why are these coercions allowed if the role signature of
Dimensional
is, as GHCi's :i tells me, nominal nominal nominal? -
Is this the intended behavior?
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | low |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | goldfire |
Operating system | |
Architecture |