[GHC] #8177: Roles for type families

[GHC]

#8177: Roles for type families
-------------------------------------+-------------------------------------
              Reporter:  simonpj     |            Owner:  goldfire
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Compiler    |          Version:  7.6.3
            Resolution:              |         Keywords:
      Operating System:              |     Architecture:  Unknown/Multiple
  Unknown/Multiple                   |       Difficulty:  Unknown
       Type of failure:              |       Blocked By:
  None/Unknown                       |  Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by dmcclean):

 Yes, my apologies Simon.

 This is actually going to be an interesting example, perhaps, because I
 learned something about this since yesterday when I wrote that comment.

 This example is slightly longer than I would like, I'm eliding a few
 things but I'm not sure exactly which details (e.g. the data family being
 associated) matter.

 {{{
 class KnownVariant (var :: Variant) where
   -- | A dimensional value, either a 'Quantity' or a 'Unit', parameterized
 by its 'Dimension' and representation.
   data Dimensional var :: Dimension -> * -> *
   -- elided: some functions to allow us to introduce and eliminate the
 quantities or units

 instance KnownVariant DQuantity where
   newtype Dimensional DQuantity d v = Quantity' v
     deriving (Eq, Ord, Enum)
   -- elided: function implementations

 instance KnownVariant (DUnit p) where
   data Dimensional (DUnit p) d v = Unit' UnitName v
   -- elided: function implementations

 data Variant = DQuantity | DUnit Prefixability
 type Quantity = Dimensional DQuantity
 type Unit p = Dimensional (DUnit p)
 }}}

 So I set up all that machinery, and then I was curious whether we could
 `coerce` in and out of the `Dimensional DQuantity d` newtype. So I thought
 that the way to find out was by asking GHCi what the role of `Dimensional`
 was. In concept it's `nominal phantom representational`, but it would be
 extremely complicated for the compiler to see that because it would have
 to examine all the (both the) instances and so forth, so I didn't know
 what to expect.

 {{{
 Numeric.Units.Dimensional.DK> :i Dimensional
 class KnownVariant (var :: Variant) where
   type role Dimensional nominal nominal nominal
   data family Dimensional (var :: Variant) ($a :: Dimension) $b
   ...
 }}}

 So I read that, and thought that it meant we were out of luck.

 But, unexpectedly to me, but undoubtedly for a reason that is quite
 obvious to someone, and this is the part I only discovered last night:

 {{{
 > let x = 3.7 :: Double
 > x
 3.7
 > let y = (coerce x) :: Mass Double
 > y
 3.7 kg
 > let x' = (coerce y) :: Double
 > x'
 3.7
 }}}

 Somehow it even seems to be OK when you abstract over the dimension with
 RankNTypes, which isn't really a need but is just something I thought to
 investigate to see if that was the difference between my expectation of
 how this would work and how it in fact did work.

 {{{
 > let f = coerce :: (forall d.Double -> Quantity d Double)
 > (f 3) :: Mass Double
 3.0 kg
 }}}

 In conclusion, I now believe that I was too hasty yesterday, and that in
 fact this ticket doesn't impact me at all.

 My sincere apologies to everyone copied on this ticket. If someone
 happened to have the time and knew the answer, it would be awesome if you
 you could help me fix my understanding about whether this should or
 shouldn't work and what the interplay with roles is, but otherwise I will
 merrily go about my business. :)

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8177#comment:20>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler