[GHC] #14111: strange error when using data families with levity polymorphism and unboxed sums and data families
GHC
ghc-devs at haskell.org
Mon Aug 21 09:55:37 UTC 2017
#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
More information about the ghc-tickets
mailing list