Opened 9 months ago

Closed 8 months ago

#13158 closed feature request (invalid)

Pattern synonyms should use type annotation information when typechecking

Reported by: lexi.lambda 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: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #13159, #11350 Differential Rev(s):
Wiki Page:

Description

With a small boatload of GHC extensions, I can write a view pattern with Data.Typeable that will simulate something like case analysis on types:

{-# LANGUAGE GADTs, PatternSynonyms, ScopedTypeVariables,
             TypeApplications, TypeOperators, ViewPatterns #-}

import Data.Typeable

viewEqT :: forall b a. (Typeable a, Typeable b) => a -> Maybe ((a :~: b), b)
viewEqT x = case eqT @a @b of
  Just Refl -> Just (Refl, x)
  Nothing -> Nothing

evilId :: Typeable a => a -> a
evilId (viewEqT @Int -> Just (Refl, n)) = n + 1
evilId (viewEqT @String -> Just (Refl, str)) = reverse str
evilId x = x

However, this is ugly. I would like to clean things up with a nice pattern synonym:

pattern EqT :: forall b a. (Typeable a, Typeable b) => (a ~ b) => b -> a
pattern EqT x <- (viewEqT @b -> Just (Refl, x))

Sadly, while this pattern typechecks, using it seems to be impossible. This program is rejected:

evilId :: Typeable a => a -> a
evilId (EqT (n :: Int)) = n + 1
evilId (EqT (str :: String)) = reverse str
evilId x = x

Specifically, it produces the following type error:

/private/tmp/wild-patterns-sandbox/library/TypeEqTest.hs:17:9: error:
    • Could not deduce (Typeable b0) arising from a pattern
      from the context: Typeable a
        bound by the type signature for:
                   evilId :: Typeable a => a -> a
        at library/TypeEqTest.hs:16:1-30
      The type variable ‘b0’ is ambiguous
    • In the pattern: EqT (n :: Int)
      In an equation for ‘evilId’: evilId (EqT (n :: Int)) = n + 1

/private/tmp/wild-patterns-sandbox/library/TypeEqTest.hs:17:14: error:
    • Could not deduce: a ~ Int
      from the context: a ~ b0
        bound by a pattern with pattern synonym:
                   EqT :: forall b a. (Typeable a, Typeable b) => a ~ b => b -> a,
                 in an equation for ‘evilId’
        at library/TypeEqTest.hs:17:9-22
      ‘a’ is a rigid type variable bound by
        the type signature for:
          evilId :: forall a. Typeable a => a -> a
        at library/TypeEqTest.hs:16:11
      Expected type: Int
        Actual type: b0
    • When checking that the pattern signature: Int
        fits the type of its context: b0
      In the pattern: n :: Int
      In the pattern: EqT (n :: Int)
    • Relevant bindings include
        evilId :: a -> a (bound at library/TypeEqTest.hs:17:1)

/private/tmp/wild-patterns-sandbox/library/TypeEqTest.hs:18:9: error:
    • Could not deduce (Typeable b1) arising from a pattern
      from the context: Typeable a
        bound by the type signature for:
                   evilId :: Typeable a => a -> a
        at library/TypeEqTest.hs:16:1-30
      The type variable ‘b1’ is ambiguous
    • In the pattern: EqT (str :: String)
      In an equation for ‘evilId’:
          evilId (EqT (str :: String)) = reverse str

/private/tmp/wild-patterns-sandbox/library/TypeEqTest.hs:18:14: error:
    • Could not deduce: a ~ String
      from the context: a ~ b1
        bound by a pattern with pattern synonym:
                   EqT :: forall b a. (Typeable a, Typeable b) => a ~ b => b -> a,
                 in an equation for ‘evilId’
        at library/TypeEqTest.hs:18:9-27
      ‘a’ is a rigid type variable bound by
        the type signature for:
          evilId :: forall a. Typeable a => a -> a
        at library/TypeEqTest.hs:16:11
      Expected type: String
        Actual type: b1
    • When checking that the pattern signature: String
        fits the type of its context: b1
      In the pattern: str :: String
      In the pattern: EqT (str :: String)
    • Relevant bindings include
        evilId :: a -> a (bound at library/TypeEqTest.hs:17:1)

I would expect the program to typecheck, since in any other context, GHC would not have any trouble inferring the type of b for each use of EqT. However, it seems that pattern synonyms do not allow me to provide any type information “in”, only get type information “out”. Is there some fundamental limitation that forces this to be the case, or is this just a missing feature?

Change History (5)

comment:1 Changed 9 months ago by lexi.lambda

comment:2 Changed 9 months ago by goldfire

Your code looks reasonable to me and should be accepted. My guess is that this is just a type-checking bug, but I've not looked at the GHC code.

comment:3 Changed 9 months ago by simonpj

Keywords: PatternSynonyms added

comment:4 Changed 9 months ago by lexi.lambda

comment:5 Changed 8 months ago by simonpj

Resolution: invalid
Status: newclosed

This is a tricky one, but I think it is behaving correctly.

Imagine desugaring it evilId like this

-- The original
-- evilId (EqT (n :: Int)) = n + 1

-- Desugars to
evilId :: Typeable a => a -> a
evilId x = case viewEqT x of
              Just (Refl, (n :: Int)) -> n + 1
              Nothing                 -> error "urk"

(The error "urk" is just a stub; in reality we arrange to fall through to the next equation, but we can ignore that here.)

This fails with

T13158.hs:31:27: error:
    • Could not deduce: a ~ Int
      from the context: b0 ~ a
        bound by a pattern with constructor:
                   Refl :: forall k (a :: k). a :~: a,
                 in a case alternative
        at T13158.hs:31:20-23

It's not a great error message, but the payload is this

  • When calling viewEqT we must choose what types to instantiate it at; say b := beta and a := alpha.
  • Now the Refl brings into scope alpha ~ beta.
  • Now, inside that Refl match, the type signature (n :: Int) tells us that we need beta ~ Int.

But beta is untouchable here (because of the equality) so we can't unify it.

That is why you needed the type application in your other version viewEqT @Int -> Just (Refl, n)

As #13159 points out, if we had type applications in patterns we could write

evilId (EqT @Int n) = ...

The ticket for that is #11350. Meanwhile I'll close this one as invalid.

Note: See TracTickets for help on using tickets.