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

5 Dec 2014

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

Comment (by tvynr):

 I just ran into something that seems at least related.  I'm trying to use
 Happy in tandem with statically typing the payload I get from different
 functions (so I don't have to do the thing the GHC parser does with
 explicit calls to unwrapping functions).  Eventually, I got the essence of
 the problem down to this MWE:

 {{{
 {-# LANGUAGE GADTs, ExistentialQuantification #-}

 module Main where

 data Token t = forall a. Token (SomeToken t a)

 data SomeToken t a = SomeToken (t a) a

 data TokenType a where
     TokLitInt :: TokenType Integer
     TokLitPlus :: TokenType ()

 -- Without the type signature, GHC 7.8.3 can't infer the type of this
 function.
 --foo :: Token TokenType -> Integer
 foo (Token (SomeToken TokLitInt x)) = x + 1
 foo _ = 0

 main :: IO ()
 main = undefined
 }}}

 The above code typechecks in GHC 7.6.3 with and without the type
 signature.  In GHC 7.8.3, it fails to typecheck (unless the type signature
 is present) with the following error message:

 {{{
     Couldn't match type ‘a’ with ‘Integer’
       ‘a’ is untouchable
         inside the constraints (a1 ~ Integer)
         bound by a pattern with constructor
                    TokLitInt :: TokenType Integer,
                  in an equation for ‘foo’
         at Test.hs:15:23-31
       ‘a’ is a rigid type variable bound by
           the inferred type of foo :: Num a => Token TokenType -> a
           at Test.hs:15:1
     Expected type: a
       Actual type: a1
     Relevant bindings include
       foo :: Token TokenType -> a (bound at Test.hs:15:1)
     In the expression: x + 1
     In an equation for ‘foo’:
         foo (Token (SomeToken TokLitInt x)) = x + 1
 }}}

 This is unfortunate for me because Happy doesn't generate type signatures
 but does, in the approach I'm using, wind up generating code that behaves
 equivalently.  Putting a type signature on the use of "x" doesn't help,
 either, though I'm guessing that this is unsurprising to those who
 understand the relevant paper better.  :)

 If you'll forgive my naiveté, it seems pretty peculiar from the
 perspective of an amateur Haskell programmer that this type isn't
 inferred; I'd think that the type variable from the two arguments of
 SomeToken would be unified by the fact that they were introduced by the
 same pattern match.  But the error message indicates two variables, "a"
 and "a1", and doesn't really seem to relate them.  Am I missing something?

 That said, I need to read the paper mentioned in this thread rather
 thoroughly now and I understand if it sounds like I'm asking for a pony.
 :)

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