[GHC] #9211: Untouchable type variable (regression from 7.6)

16 Jun 2014


      #9211: Untouchable type variable (regression from 7.6)
------------------------------------+-------------------------------------
       Reporter:  simonpj           |             Owner:
           Type:  bug               |            Status:  new
       Priority:  normal            |         Milestone:
      Component:  Compiler          |           Version:  7.8.2
       Keywords:                    |  Operating System:  Unknown/Multiple
   Architecture:  Unknown/Multiple  |   Type of failure:  None/Unknown
     Difficulty:  Unknown           |         Test Case:
     Blocked By:                    |          Blocking:
Related Tickets:                    |
------------------------------------+-------------------------------------
 Oleg says: what used to type check in GHC 7.4.1 (and I think
 in 7.6.2, although I no longer have access to that version) fails in
 GHC 7.8.2.

 The following program type-checks with GHC 7.4.1 and GHC 7.8.2:
 {{{
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}

 module T where

 foo :: (forall f g. (Functor f) => f a -> f b) -> [a] -> [b]
 -- foo :: (forall f g. (Functor f, g ~ f) => g a -> g b) -> [a] -> [b]
 foo tr x = tr x

 t = foo (fmap not) [True]
 }}}
 The following code (which differs only in the signature of foo)
 {{{
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}

 module T where

 -- foo :: (forall f g. (Functor f) => f a -> f b) -> [a] -> [b]
 foo :: (forall f g. (Functor f, g ~ f) => g a -> g b) -> [a] -> [b]
 foo tr x = tr x

 t = foo (fmap not) [True]
 }}}

 type-checks with 7.4.1 but not with 7.8.2. The latter reports the
 error
 {{{
     Couldn't match type `b' with `Bool'
       `b' is untouchable
         inside the constraints (Functor f, g ~ f)
         bound by a type expected by the context:
                    (Functor f, g ~ f) => g Bool -> g b
         at /tmp/t.hs:12:5-25
       `b' is a rigid type variable bound by
           the inferred type of t :: [b] at /tmp/t.hs:12:1
     Expected type: Bool -> b
       Actual type: Bool -> Bool
     Relevant bindings include t :: [b] (bound at /tmp/t.hs:12:1)
     In the first argument of `fmap', namely `not'
     In the first argument of `foo', namely `(fmap not)'
 }}}
 Giving `t` the type signature `[Bool]` fixes the problem. Alas, I come
 across the similar untouchable error in situations where giving the type
 signature is quite difficult (in local bindings, with quite large types).

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