Opened 2 years ago

Closed 2 years ago

#5600 closed bug (invalid)

Instantiation of a rank 2 type fails for type synonyms

Reported by: paba Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.2.1
Keywords: Cc: paba@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty:
Test Case: Blocked By:
Blocking: Related Tickets:

Description

The instantiation of a rank 2 type with a type containing type synonyms that rearrange or omit type variables fails.

For example, consider the following function:

mapR :: Functor f => (forall a. g a -> b) -> f (g a) -> f b
mapR f t = fmap f t

Now we want to instantiate the type variable g in the above type:

data F a = F a
type G a = F a

mapG :: Functor f =>  (forall a. G a -> b) -> f (G a) -> f b
mapG f t = mapR f t

This works fine. But if we change the definition of the type synonym G to

type G a = F ()

we get the following error message:

/home/paba/code/bug.hs:11:17:
    Could not deduce (a1 ~ ())
    from the context (Functor f)
      bound by the type signature for
                 mapG :: Functor f => (forall a1. G a1 -> b) -> f (G a) -> f b
      at /home/paba/code/bug.hs:11:1-19
      `a1' is a rigid type variable bound by
           a type expected by the context: F a1 -> b
           at /home/paba/code/bug.hs:11:12
    Expected type: F a -> b
      Actual type: G a0 -> b
    In the first argument of `mapR', namely `f'
    In the expression: mapR f t

This only happens for rank 2 types. If we change the type of mapR by removing the quantifier, the instantiation of the type of mapR succeeds.

Change History (3)

comment:1 Changed 2 years ago by paba

  • Cc paba@… added

comment:2 Changed 2 years ago by kosmikus

AFAICS, GHC is correct to reject this program. You are trying to pass a function of type

forall a. F () -> b

in a position where

forall a. g a -> b

is expected.

comment:3 Changed 2 years ago by simonpj

  • Resolution set to invalid
  • Status changed from new to closed

Ian's right.

Simon

Note: See TracTickets for help on using tickets.