[GHC] #12362: don't complain about type variable ambiguity when the expression is parametrically polymorphic

3 Jul 2016

      #12362: don't complain about type variable ambiguity when the expression is
parametrically polymorphic
-------------------------------------+-------------------------------------
           Reporter:  rwbarton       |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  low            |         Milestone:
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I'm not sure this is really a good idea, but it did come up in practice.
 Consider the following rather contrived program:
 {{{#!hs
 {-# LANGUAGE TypeFamilies, RankNTypes, ScopedTypeVariables,
              AllowAmbiguousTypes, TypeApplications #-}

 module E where

 type family T a
 type instance T Int = Char
 type instance T String = Char
 type instance T Bool = ()

 newtype FT a = FT [T a]

 m :: forall a. (forall x. T x -> Int) -> FT a -> [Int]
 m f (FT xs) = map f xs
 }}}
 GHC rejects it with the error:
 {{{
 E.hs:14:21: error:
     • Couldn't match type ‘T a’ with ‘T x0’
       Expected type: [T x0]
         Actual type: [T a]
       NB: ‘T’ is a type function, and may not be injective
       The type variable ‘x0’ is ambiguous
     • In the second argument of ‘map’, namely ‘xs’
       In the expression: map f xs
       In an equation for ‘m’: m f (FT xs) = map f xs
     • Relevant bindings include
         xs :: [T a] (bound at E.hs:14:9)
         m :: (forall x. T x -> Int) -> FT a -> [Int] (bound at E.hs:14:1)
 }}}
 The problem seems to be that GHC doesn't know at what type to instantiate
 `f`, because it can't conclude from the argument of `f` being `T a` that
 the type parameter of `f` needs to be `x`. In fact, `T` here really is not
 injective, so if `a` is `Int`, `x` could just as well be `String`.

 However, in this case the ambiguity doesn't actually matter. If `f @Int`
 and `f @String` have the same type because `T Int ~ T String`, then they
 are actually the same value too by parametricity, because there is no
 class constraint on `x`. Since GHC prints a message saying that `T` is not
 known to be injective, it sounds like it knows about the possible solution
 `x0 = a`. So it could just pick it, and accept the original program.

 With TypeApplications I can just specify the intended value of `x` by
 writing
 {{{
 m f (FT xs) = map (f @a) xs
 }}}
 which is a reasonable workaround in my real use case also. Interestingly I
 can't seem to achieve the same thing without TypeApplications without
 adding a proxy argument to `f`, which I don't much want to do.

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