Opened 11 months ago
Closed 10 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 11 months ago by
Related Tickets: | → #13159 |
---|
comment:2 Changed 11 months ago by
comment:3 Changed 11 months ago by
Keywords: | PatternSynonyms added |
---|
comment:4 Changed 11 months ago by
Related Tickets: | #13159 → #13159, #11350 |
---|
comment:5 Changed 10 months ago by
Resolution: | → invalid |
---|---|
Status: | new → closed |
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; sayb := beta
anda := alpha
. - Now the
Refl
brings into scopealpha ~ beta
. - Now, inside that
Refl
match, the type signature(n :: Int)
tells us that we needbeta ~ 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.
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.