[GHC] #9171: Can't match type family with kind polymorphism

[GHC]

#9171: Can't match type family with kind polymorphism
----------------------------+----------------------------------------------
       Reporter:            |             Owner:
  MikeIzbicki               |            Status:  new
           Type:  bug       |         Milestone:
       Priority:  normal    |           Version:  7.8.2
      Component:  Compiler  |  Operating System:  Unknown/Multiple
       Keywords:            |   Type of failure:  GHC rejects valid program
   Architecture:            |         Test Case:
  Unknown/Multiple          |          Blocking:
     Difficulty:  Unknown   |
     Blocked By:            |
Related Tickets:            |
----------------------------+----------------------------------------------
 Create a module with the following code:

 {{{
 data Base

 type family GetParam (p::k1) (t::k2) :: k3

 type instance GetParam Base t = t
 }}}

 It loads into GHCi just fine.  But when we run:

 {{{
 ghci> :t undefined :: GetParam Base (GetParam Base Int)
 }}}

 we get an error

 {{{
 <interactive>:1:14:
     Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
                 with actual type ‘GetParam Base (GetParam Base Int)’
     NB: ‘GetParam’ is a type function, and may not be injective
     The type variable ‘k0’ is ambiguous
     In the ambiguity check for: GetParam Base (GetParam Base Int)
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In an expression type signature: GetParam Base (GetParam Base Int)
     In the expression: undefined :: GetParam Base (GetParam Base Int)
 }}}

 If we modify the module by either

 1) set `k3` to `k2`, `k1`, or any concrete kind

 or

 2) set `k2` to any concrete kind

 then the ghci snippet will type check just fine.

 I assume that this is a mistake, and that the original code should work
 just fine.  If there is some reason, however, why the program would be
 unsound, then the error message should be made a bit more informative.
 The claim is that the kind `k0` is ambiguous, but it doesn't appear
 anywhere in my code!  In my full program, it took me a long time to narrow
 down that this was the source of the problem.

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