Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,396
    • Issues 4,396
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 378
    • Merge Requests 378
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #12362

Closed
Open
Opened Jul 03, 2016 by rwbarton@trac-rwbarton

don't complain about type variable ambiguity when the expression is parametrically polymorphic

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
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#12362