Regression around pattern synonyms and higher-rank types

GHC 8.0.1 accepts, but HEAD rejects:

{-# LANGUAGE PatternSynonyms, RankNTypes, ViewPatterns #-}

module Bug where

pattern P :: (forall a. a -> a) -> String
pattern P x <- (\ _ -> id -> x)

(Sidenote: kudos to the parser on figuring out my view pattern.)

HEAD gives this error:

Bug.hs:6:30: error:
    • Couldn't match expected type ‘forall a. a -> a’
                  with actual type ‘a0 -> a0’
    • In the declaration for pattern synonym ‘P’
    • Relevant bindings include x :: a0 -> a0 (bound at Bug.hs:6:30)

The code looks correct to me.

Trac metadata

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

changed weight to 5

added Tbug Trac import typechecker labels

What makes you say it's correct?

Consier

f :: String -> Int
f ( (\_ -> id) -> (x :: forall a. a->a) ) = 3

This too is rejected with

T12820.hs:10:20: error:
    * Couldn't match expected type `a0 -> a0'
                  with actual type `forall a. a -> a'
    * When checking that the pattern signature: forall a. a -> a
        fits the type of its context: a0 -> a0
      In the pattern: x :: forall a. a -> a
      In the pattern: (\ _ -> id) -> (x :: forall a. a -> a)

Suppose we are inferring the type of f -> p. W could either

• Infer the type of f, and use that to check the type of pattern p, or
• Infer the type of p, and use that to check the type of f (actually it only fixes teh result type of f but still.

We use the first alternative, but perhpas the second makes more sense.

Fair enough. But the problem persists even with a type signature on the pattern:

pattern P x <- (((\ _ -> id) :: forall b c. b -> c -> c) -> x)

Interestingly, adding the type signature fails in GHC 8.0.1 as well as HEAD.

Hmm. Works ok if you put the forall after the arrow

pattern P x <- (((\ _ -> id) :: forall b. b -> forall c. c -> c) -> x)

Reason: we infer the type of f, and then try to decompose and arrow, instantiating if necessary. But we don't re-generalise.

I suppose we could but this is a pretty exotic corner and it's not keeping me awake at night.

Simon

assigned to @rae

Maybe this is what kept me awake last night. Or maybe it was my cat who felt the need to lovingly stroke my face roughly hourly. Until she was banished to the kitchen.

No, I'm not overly bothered by this. But it is subtly wrong, according to any bidirectional accounting of a type system that accommodates view patterns and has principal types.

I'll put this in my queue. At the bottom. :)

This regression was introduced somewhere between commit 45bfd1a6 (Refactor typechecking of pattern bindings) and 9417e579 (Refactor occurrence-check logic).

(I'm 90% sure it's 45bfd1a6, but I can't say with certainty because that commit was in the middle of a slew of commits which didn't compile correctly until 9417e579.)

added Pnormal label