Re: [GHC] #9633: PolyKinds in 7.8.2 vs 7.8.3

26 Sep 2014

      #9633: PolyKinds in 7.8.2 vs 7.8.3
-------------------------------------+-------------------------------------
              Reporter:  crockeea    |            Owner:
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Compiler    |          Version:  7.8.3
            Resolution:              |         Keywords:  PolyKinds
      Operating System:              |     Architecture:  Unknown/Multiple
  Unknown/Multiple                   |       Difficulty:  Unknown
       Type of failure:  GHC         |       Blocked By:
  rejects valid program              |  Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Here is what is happening.

  * Between 7.8.2 and 7.8.3, I fixed #8985.

  * That meant that when typechecking `go` we get a deferred equality
 constraint `v ~ alpha`, where `alpha` is a unification variable, but
 untouchable.  (Before it was (wrongly) solved on the fly by unifiying an
 untouchable kind variable.)

  * Because `TypeFamilies` and `MonoLocalBinds` are not on, we try to
 generalise `go`. That give it a signature like `go :: (Monad m, PrimState
 m ~ PrimState s) => ...blah...`

  * Hence we get a residual unsolved implication constraint like `(Monad m,
 PrimState m ~ PrimState s) => v ~ alpha`.

  * We can't float `v ~ alpha` out of the implication because there's an
 equality in the "givens".

  * So it never gets solved.

 HEAD complains instead:
 {{{
 T9633.hs:17:7:
     Illegal equational constraint PrimState m ~ PrimState s
     (Use GADTs or TypeFamilies to permit this)
     When checking that ‘go’ has the inferred type
       go :: forall (m :: * -> *).
             (Monad m, PrimState m ~ PrimState s) =>
             Int -> m ()
 }}}
 And when you switch on `TypeFamilies` that switches on `MonoLocalBinds`
 which in turn means that we don't attempt to generalise `go`, and the
 program compiles fine.

 Bottom line: I don't expect most users to make sense of the above
 explanation, but HEAD points you in the right direction.

 It's an instructive case, but I don't propose to take any new action.

 Simon

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9633#comment:8
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler