GitLab

I'm not sure this is really a good idea, but it did come up in practice. Consider the following rather contrived program:

{-# 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.

Trac metadata

Trac field	Value
Version	8.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	low
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture