Opened 8 months ago

Last modified 8 months ago

#12975 new bug

Suggested type signature for a pattern synonym causes program to fail to type check

Reported by: ocharles Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1
Keywords: PatternSynonyms Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Take the following program:

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

import Data.Typeable

data T where
  MkT :: Typeable a => a -> T

pattern Cast a <- MkT (cast -> Just a)

When compiled with -Wall, GHC rightly prompts about a missing signature on Cast:

    Top-level binding with no type signature:
      Cast :: forall b. Typeable b => forall a. Typeable a => b -> T

However, using this suggested type signature causes the program to fail to type check:

     Could not deduce (Typeable a0)
        arising from the "provided" constraints claimed by
          the signature of Cast
      from the context: Typeable a
        bound by a pattern with constructor:
                   MkT :: forall a. Typeable a => a -> T,
                 in a pattern synonym declaration
        at ../foo.hs:9:19-38
      In other words, a successful match on the pattern
        MkT (cast -> Just a)
      does not provide the constraint (Typeable a0)
      The type variable a0 is ambiguous
     In the declaration for pattern synonym Cast

Change History (5)

comment:1 Changed 8 months ago by ocharles

I actually believe the correct type of this pattern is

pattern Cast :: () => Typeable a => a -> T
pattern Cast a <- MkT (cast -> Just a)

But this is also rejected:

    • Could not deduce (Typeable a0) arising from a use of ‘cast’
      from the context: Typeable a
        bound by a pattern with constructor:
                   MkT :: forall a. Typeable a => a -> T,
                 in a pattern synonym declaration
        at ../foo.hs:9:19-38
      The type variable ‘a0’ is ambiguous
    • In the pattern: cast -> Just a
      In the pattern: MkT (cast -> Just a)
      In the declaration for pattern synonym ‘Cast’

I may be wrong with that type though.

comment:2 Changed 8 months ago by mpickering

Keywords: PatternSynonyms added; patternsynonyms removed

The type signature you are looking for is...

pattern Cast :: Typeable b => b -> T
pattern Cast a <- MkT (cast -> Just a)

cast has type (Typeable a, Typeable b) => a -> Maybe b, as MkT provides Typeable a for us, we require Typeable b in order to use the function.

The inferred type is still wrong in HEAD. Thanks!

comment:3 Changed 8 months ago by ocharles

If I only supply one context, which context am I supplying? The provided one, or the required one? That is, are you suggesting pattern Cast :: () => Typeable b => ... or pattern Cast :: Typeable b => () => ...?

comment:4 Changed 8 months ago by mpickering

The required one.

req => t is the same as req => () => t. This is different from the first implementation, we changed it last release.

comment:5 Changed 8 months ago by simonpj

The reported type is sort of right:

Cast :: forall b. Typeable b => forall a. Typeable a => b -> T

That is, you can match a value of any type b provided it is typeable. So

f (Cast x) = rhs

means pretty much

f (MkT y) = case cast y of 
              Just x -> rhs

Inside rhs we have access to the Typeable a constraint bound by MkT; that's what the Typeable a constraint in the inferred type is saying.

But this Typeable a provided constraint is no use to rhs because we have no values of type a. So Matthew's type is less confusing

pattern Cast :: Typeable b => b -> T

Offering useless constraints is bad enough; but worse, as you report, it's rejected as ambiguous (for the same reason) if you specify it in a user signature. That is indeed confusing.

What I can't see is a robust and convenient way to eliminate the unnecessary constraints and existential variables.

Note: See TracTickets for help on using tickets.