[GHC] #9223: Type equality makes type variable untouchable

[GHC]

#9223: Type equality makes type variable untouchable
--------------------------------------------+------------------------------
        Reporter:  Feuerbach                |            Owner:
            Type:  bug                      |           Status:  new
        Priority:  normal                   |        Milestone:
       Component:  Compiler (Type checker)  |          Version:  7.8.2
      Resolution:                           |         Keywords:
Operating System:  Unknown/Multiple         |     Architecture:
 Type of failure:  None/Unknown             |  Unknown/Multiple
       Test Case:                           |       Difficulty:  Unknown
        Blocking:                           |       Blocked By:
                                            |  Related Tickets:
--------------------------------------------+------------------------------

Comment (by simonpj):

 GHC is being schizophrenic about an interesting design choice here.  The
 issue is this.

 When typechecking `x2`'s RHS, we assume that the RHS has type `alpha`, for
 some fresh unification variable `alpha`, and generate constraints from the
 RHS, giving the constraint:
 {{{
 forall m. (Monad m, TF m  ~ ())       -- Comes from run2's type
        => (m alpha ~ m (),            -- Matching result of (return ())
 with expected type (m alpha)
            Monad m)                   -- Call of return
 }}}
 That leads to the constraint `(alpha ~ ())`, but underneath an implication
 constraint that has an equality (like a GADT) in it.  So !OutsideIn
 refrains from unifying `alpha`.

 Then GHC tries to infer a type for `x2` anyway, getting (essentially)
 {{{
 x2 :: forall a. (a ~ ()) => a
 }}}
 where we have decided to quantify over `alpha` to `a`.  Finally we end up
 reporting the insoluble constraint `(a ~ alpha)`.

 So the question is: what error message would you like to see? This
 "untouchable" stuff is a bit disconcerting, so we could say this:
 {{{
     Couldn't match expected type ‘a’ with actual type ‘()’
       ‘a’ is a rigid type variable bound by
           the inferred type of x2 :: forall a. a at untouchable.hs:15:1
     Relevant bindings include x2 :: a (bound at untouchable.hs:15:1)
     In the first argument of ‘return’, namely ‘()’
     In the first argument of ‘run2’, namely ‘(return ())’
 }}}
 Here you get to see the inferred type of `x2`. (Side note: actually GHC
 currently prints `the inferred type of x2 :: a`, suppressing the `forall`,
 but in this context I suspect we should print the `forall` regardless of
 `-fprint-explicit-foralls`.  I'll make that change anyway unless anyone
 yells.)

 A merit of this error message is that if you, the programmer, give `x2`
 that type signature `x2 :: forall a. a`, then indeed that is very much the
 message that you'll get.  But I suppose it leaves open the question of
 '''why''' GHC inferred that type for `x2`.

 Alternatively we could give you
 {{{
     Couldn't match expected type ‘a’ with actual type ‘()’
       ‘a’ is untouchable
         inside the constraints (Monad m, TF m ~ ())
         bound by a type expected by the context:
                    (Monad m, TF m ~ ()) => m a
         at untouchable.hs:15:6-21
     Relevant bindings include x2 :: a (bound at untouchable.hs:15:1)
     In the first argument of ‘return’, namely ‘()’
     In the first argument of ‘run2’, namely ‘(return ())’
 }}}
 which perhaps exposes a bit more of the mechanism of !OutsideIn, and has
 the merit of displayin the constraint(s) that make it untouchable.

 Which would you prefer?  Currently GHC displays both, which I agree is
 confusing.

 Simon

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