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

[GHC]

#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:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Consider
 {{{
 data instance T a [a] where
   T1 :: Int -> T Bool [Bool]
   T2 :: Char -> T Bool [Char]  -- Wrong
   T3 :: p -> T p q             -- Wrong
 }}}
 We want to ensure that the result type of each data constructor is a
 substitution instance of the `T a [a]` in the head.  `T2` isn't, so it's
 rejected.  Ditto `T3`

 But this ticket points out that the user-written signature for the data
 constructor has invisible (and hence under-specified) kind arguments.  We
 want those kind arguments to conform to the shape of the head too.

 One way to do this might be, when kind-checking the type signature for a
 data constructor,
  * Instantiate the head shape with fresh unification variables
  * Unify it with the result type of the data constructor
 That would force the shapes to match, and would instantiate any kind
 variables appropriately.

 I'm not sure what we'd do with the kind coercion that this unification
 would return; but it smells to me like the right thing to do.

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