#6049: Kind variable generalization error in GADTs
----------------------------------------+-----------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.5
Keywords: PolyKinds | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: GHC rejects valid
program
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
----------------------------------------+-----------------------------------
Comment(by goldfire):
Actually, I think you've over-generalized the problem. As I see it, the
kinds for {{{SMaybe}}} in both constructors are the same (modulo kind
variables --- but maybe that's the issue). In any case, the error still
comes up when I omit the {{{SJust}}} constructor. Fortunately, in both
this case and in my original, larger case, the problem goes away when I
avoid GADT syntax, so this isn't holding me up any longer.
As for your description above, I don't fully understand why the treatment
of the two syntax forms have to be different. In the original {{{SMaybe}}}
case, I propose this: Read {{{SMaybe}}}'s kind from the user-supplied
signature, and then infer {{{SMaybe}}}'s kind from the constructor
definitions. Notice that all three kinds are the same, modulo names of
kind variables, so we unify the variables and are done. Is there some
detail I'm missing here? Does kind variable unification in that way not
exist yet? I recognize that the case above is very simple, in that the
kinds to be compared are all structurally identical and that the general
case may require matching one kind variable against some structural
component, possibly containing other variables, in another kind. However,
my intuition is that this manner of unification must already exist
somewhere. Am I wrong?
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6049#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
