#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