[GHC] #9725: Constraint deduction failure

[GHC]

#9725: Constraint deduction failure
-------------------------------------+-------------------------------------
              Reporter:  heisenbug   |            Owner:
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Compiler    |          Version:  7.8.3
  (Type checker)                     |         Keywords:
            Resolution:              |     Architecture:  Unknown/Multiple
      Operating System:              |       Difficulty:  Unknown
  Unknown/Multiple                   |       Blocked By:
       Type of failure:  GHC         |  Related Tickets:
  rejects valid program              |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by heisenbug):

 Replying to [comment:6 simonpj]:
 ... snip ...
 > The pattern-match on `Mb` indeed yields the given equality `ent::k ~
 M::Bool`.  But we can't ''use'' that unless we know that `k~Bool` and,
 until Richard implements kind-level equalities, we don't know that.

 But isn't this just plain ''kind inference'' as we have it today?

 >
 > The "restricted kind signature" de-polymorphises" it, which is all you
 need to make it work.

 Right, that's what I figured. But in my ''actual'' code I have
 {{{
 data En = M Bool | Ind Nat -- etc.

 data Fac :: En -> * where
    Mo :: Kn (M b) => Fac (M b)
    Odu :: Kn (Ind n) => Fac (Ind n)
    -- etc.
 }}}

 And the pattern match in `h` goes over these, so I *need* the poly-
 kindedness. It would let me consolidate a bunch of otherwise identical
 functions (modulo constructor names).

 >
 > Richard: you should add this to your test suite for kind-level
 equalities!  Is there a wiki page for this?  Is it
 [wiki:DependentHaskell]?  I suspect not.
 >
 > Simon

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