[GHC] #9580: Possible excessive leniency in interaction between coerce and data families?

11 Sep 2014

      #9580: Possible excessive leniency in interaction between coerce and data
families?
-------------------------------------+-------------------------------------
       Reporter:  dmcclean           |                   Owner:
           Type:  bug                |                  Status:  new
       Priority:  low                |               Milestone:
      Component:  Compiler (Type     |                 Version:  7.8.3
  checker)                           |        Operating System:
       Keywords:                     |  Unknown/Multiple
   Architecture:  Unknown/Multiple   |         Type of failure:
     Difficulty:  Unknown            |  None/Unknown
     Blocked By:                     |               Test Case:
Related Tickets:                     |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------
 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:

 1) Why are these coercions allowed if the role signature of `Dimensional`
 is, as GHCi's :i tells me, nominal nominal nominal?

 2) Is this the intended behavior?

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9580
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler