Re: [GHC] #14111: strange error when using data families with levity polymorphism and unboxed sums and data families

24 Jul 2018

      #14111: strange error when using data families with levity polymorphism and unboxed
sums and data families
-------------------------------------+-------------------------------------
        Reporter:  carter            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:  13737             |             Blocking:
 Related Tickets:  #14457            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Recording some thoughts from a conversation with Richard and Simon:

 * The fact that programs like in the one in comment:23 won't compile is
 OK. In general, the type of a data constructor is quite restricted
 compared to other type signatures, and there already precedent for
 disallowing type synonyms in certain spots of data constructors. For
 instance, GHC rejects this example (from #7494):

 {{{#!hs
 data Steps s y where
   Yield :: y -> FK s y -> FK s y
   Done  :: Steps s y
 type FK s y = s -> Steps s y
 }}}

   So it's perhaps not so unusual for GHC to reject the example from
 comment:23 as well. But this should be documented in the users' guide.
 (Should this bullet point have its own ticket?)
 * The code in comment:14 is slightly unusual in that we call `unifyType`,
 but immediately throw away the coercion that it returns. But this is also
 OK—there is an invariant that the coercion returned here will always be
 reflexive. As evidence for this claim, consider the following example:

 {{{#!hs
 type family F a
 type instance F Char = [Bool]

 data family T a b
 data instance T a [a] where
   MkT :: T Bool (F Char)
 }}}

   Compiling `MkT` should require a //non//-reflexive coercion in order to
 cast its return type `T Bool [Bool]` to `T Bool (F Char)`. But we disallow
 such shenanigans in `checkValidDataCon`, which checks that the type of a
 data constructor really is an instance of the parent type (//without//
 reducing any type families). Therefore, the shape of the data constructor
 return type must be the same as the shape of the parent type, so any
 coercion between the two must be reflexive.

   This subtlety should at least be documented. (Ideally, we'd add an
 `ASSERT`ion for it too, but this would be tricky to do in `tcConDecl`, and
 the alternative of stashing the coercion in `MkDataCon` only to check it
 later in the code if `ASSERT`ions are enabled is rather ghastly.)

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14111#comment:26
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler