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

[GHC]

#9580: Possible excessive leniency in interaction between coerce and data
families?
-------------------------------------+-------------------------------------
              Reporter:  dmcclean    |            Owner:  simonpj
                  Type:  bug         |           Status:  closed
              Priority:  low         |        Milestone:
             Component:  Compiler    |          Version:  7.8.3
  (Type checker)                     |         Keywords:
            Resolution:  fixed       |     Architecture:  Unknown/Multiple
      Operating System:              |       Difficulty:  Unknown
  Unknown/Multiple                   |       Blocked By:
       Type of failure:              |  Related Tickets:
  None/Unknown                       |
             Test Case:  indexed-    |
  types/should_fail/T9580            |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by dfeuer):

 Replying to [comment:8 dmcclean]:
 > I think I may have been confused for 2 different reasons.
 >
 > First, I forgot that we are coercing in your example from Dimensional
 Int Double -> Double, which should work according to rule 2 in figure 2. I
 had it mixed up with converting from Dimensional Int Double -> Dimensional
 Int x (where there is a coercion from Double to x).
 >
 > Second, it doesn't appear to actually be possible to export the
 Quantity' constructor from the defining module at all. (If I put it in the
 export list, GHCi tells me that it isn't in scope even though it is and I
 checked the spelling three times.) So the scenario I was thinking of isn't
 possible for that reason too; I hadn't realized that this was a rule.
 >
 > I now think that with the change you made everything is correct, sorry
 for the confusion.

 Did you use the proper export syntax, `Dimensional (Quantity')`? That's
 supposed to work. If you didn't get an unknown whatever error when
 exporting `Quantity'` from the defining module, I'm ''guessing'' that it
 exported the `Quantity'` ''type'' (produced by `DataKinds`) rather than
 the data constructor. I don't really know how that extension is supposed
 to work with module exports though.

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