[GHC] #12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables)
#12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler | Version: 7.10.3 (Type checker) | Keywords: GADTs, | Operating System: Unknown/Multiple ScopedTypeVariables | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs data Exp a where Tru :: Ty Bool eval :: Exp a -> a eval Tru = True }}} Works fine, as does {{{#!hs eval :: Exp a -> a eval (Tru :: Exp _) = True }}} But {{{#!hs eval :: Exp a -> a eval (Tru :: Exp Bool) = True }}} doesn't, is this an intended design of GADTs/ScopedTypeVariables that the type equality constraint isn't in scope in the type signature of the pattern match, I would like to match on an existential type in my own code: {{{#!hs compile (ArrIx arr index :: Exp (Sca elt)) = do ... }}} It can be worked around by writing: {{{#!hs eval a@Tru = case a :: Exp Bool of }}} but for my own code it seems I must write {{{#!hs compile uuu@(ArrIx arr index :: Exp a) = do case uuu :: (a ~ Sca elt) => Exp (Sca elt) of }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12018 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: GADTs, Resolution: | ScopedTypeVariables Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Hm, the type variable `elt` doesn't get brought into scope. Maybe because it's existential -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12018#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: GADTs, Resolution: | ScopedTypeVariables Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): I think this would largely be solved by #11350, {{{#!hs eval (ArrIx @_ @elt arr index) = do ... }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12018#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: GADTs, Resolution: | ScopedTypeVariables Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
Is this an intended design of GADTs/ScopedTypeVariables that the type equality constraint isn't in scope in the type signature of the pattern match
Yes, it is. The type equalities are available only "after" the match. For your second point I need a more complete example. To bind an existential you need a pattern type sig. Eg {{{ data T where MkT :: a -> ([a]->Int) -> T f (MkT (x :: a) f) = f ([x,x] :: [a]) }}} The pattern signature `(x :: a)` binds `a`. Currently that's the only way to bind an existential type variable. #11350 would be a good alternative. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12018#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: GADTs, Resolution: | ScopedTypeVariables Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12018#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: GADTs, Resolution: | ScopedTypeVariables Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:3 simonpj]:
Yes, it is. The type equalities are available only "after" the match.
I must admit that I also find this behavior quite counterintuitive. I stumbled into this when I tried typechecking this code: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} module Bug where data family Sing (a :: k) data instance Sing (z :: [a]) where SNil :: Sing '[] SCons :: Sing x -> Sing xs -> Sing (x ': xs) fl :: forall (l :: [a]). Sing l -> Sing l fl SNil = SNil fl (SCons (x :: Sing x) (xs :: Sing xs) :: Sing (x ': xs)) = SCons x xs }}} {{{ GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:17:5: error: • Couldn't match type ‘l’ with ‘x : xs’ ‘l’ is a rigid type variable bound by the type signature for: fl :: forall a1 (l :: [a1]). Sing l -> Sing l at Bug.hs:15:1-41 Expected type: Sing l Actual type: Sing (x : xs) • When checking that the pattern signature: Sing (x : xs) fits the type of its context: Sing l In the pattern: SCons (x :: Sing x) (xs :: Sing xs) :: Sing (x : xs) In an equation for ‘fl’: fl (SCons (x :: Sing x) (xs :: Sing xs) :: Sing (x : xs)) = SCons x xs • Relevant bindings include fl :: Sing l -> Sing l (bound at Bug.hs:16:1) | 17 | fl (SCons (x :: Sing x) (xs :: Sing xs) :: Sing (x ': xs)) = SCons x xs | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Bug.hs:17:62: error: • Could not deduce: l ~ (x1 : xs1) from the context: (x : xs) ~ (x1 : xs1) bound by a pattern with constructor: SCons :: forall a (x :: a) (xs :: [a]). Sing x -> Sing xs -> Sing (x : xs), in an equation for ‘fl’ at Bug.hs:17:5-39 ‘l’ is a rigid type variable bound by the type signature for: fl :: forall a1 (l :: [a1]). Sing l -> Sing l at Bug.hs:15:1-41 Expected type: Sing l Actual type: Sing (x : xs) • In the expression: SCons x xs In an equation for ‘fl’: fl (SCons (x :: Sing x) (xs :: Sing xs) :: Sing (x : xs)) = SCons x xs • Relevant bindings include xs :: Sing xs (bound at Bug.hs:17:26) x :: Sing x (bound at Bug.hs:17:12) fl :: Sing l -> Sing l (bound at Bug.hs:16:1) | 17 | fl (SCons (x :: Sing x) (xs :: Sing xs) :: Sing (x ': xs)) = SCons x xs | ^^^^^^^^^^ }}} That doesn't typecheck, and yet this does: {{{#!hs fl :: forall (l :: [a]). Sing l -> Sing l fl SNil = SNil fl (SCons (x :: Sing x) (xs :: Sing xs) :: Sing l) = SCons x xs }}} Why not? After all, GHC is smart enough to know how to bind the existentially quantified variables `x` and `xs`, so why can't it conclude that `l ~ x ': xs` from the GADT pattern match? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12018#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: GADTs, Resolution: | ScopedTypeVariables Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
Why not?
Because until you have matched on `SCons` we don't have `l ~ x:xs`. I think you are thinking that, because the type signature is "to the right" of the match, you can take advantage of it. But in fact it's more like the type signature encloses the pattern, so it's more like this {{{ fl (Sing (x ': xs) ::: SCons (x :: Sing x) (xs :: Sing xs)) = SCons x xs }}} Here I've used `ty ::: Pat` to put a type sig syntactically "before" the pattern. Now perhaps you would not expect to have matched yet? What about this {{{ g (Just [SCons x xs] :: Maybe [Sing (a ': as)]) = ... }}} presumably you want the pattern to match deeply first. To put it another way, we currently [https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-580003.1... explain pattern matching in the Haskell report] via simple case expressions. Currently we have {{{ case v of ( p::ty -> e1; _ -> e2 } ---> case (v::ty) of { p -> e2; _ -> e2 } }}} But I suppose we could say something like {{{ case v of ( p::ty -> e1; _ -> e2 } ----> case v of { p -> let (v2::ty) = v in e1 ; _ -> e2 } }}} where the type signature is not applied until after the match. I can't say I'm terribly fired up about this. I'm not sure how easy it'd be to match the signature "after" the match. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12018#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
Because until you have matched on `SCons` we don't have `l ~ x:xs`. I
#12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: GADTs, Resolution: | ScopedTypeVariables Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:6 simonpj]: think you are thinking that, because the type signature is "to the right" of the match, you can take advantage of it. The position of the type signature has nothing to do with my confusion. I'm confused because it's been drilled into my skull that the act of pattern matching on a GADT constructor in a case changes the typing rules (or, more precisely, it introduces new given constraints) for that case. The fact that I can use these given constraints for the types of subpatterns of `SCons ...`, but for the type of the `SCons ...` pattern itself, feels oddly disjointed. To highlight the strangeness of this further, you can do what I desire simply by adding another `case` expression: {{{#!hs fl :: forall (l :: [a]). Sing l -> Sing l fl SNil = SNil fl a@(SCons (x :: Sing x) (xs :: Sing xs)) = case a of (a :: Sing (x ': xs)) -> SCons x xs }}} I'd rather cut out of the middleman and just put that `Sing (x ': xs)` type directly on the `SCons ...` pattern.
To put it another way, we currently [https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-580003.1... explain pattern matching in the Haskell report] via simple case expressions. Currently we have {{{ case v of ( p::ty -> e1; _ -> e2 } ---> case (v::ty) of { p -> e2; _ -> e2 } }}}
I'm not sure where you got that rule from in the link you provided. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12018#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: GADTs, Resolution: | ScopedTypeVariables Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
it's been drilled into my skull that the act of pattern matching on a GADT constructor in a case changes the typing rules
Correct -- but it only brings those constraints into scope in ''parts'' of the program. For example {{{ data T a where TBool :: TBool TOther :: T a f :: a -> T a -> Int f True TBool = 3 -- Rejected g :: T a -> a -> Int g TBool True = 3 -- Accepted }}} `f` is rejected because pattern matching goes left-to-right and outside- in. So when we meet the `True` we are not in the scope of `a~Bool`. But `g` is fine. In the case of a type signature, when matching `(p :: ty)` we first meet `ty` and only then match `p`. You want to match `p` and only then match `ty` with the refined type of the pattern. But currently `ty` signature may restrict the type of the pattern; I'm not sure that would be so easy if the signature was only matched after matching the pattern. In short, I don't see an easy, compositional way to give you what you want. Maybe someone else does. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12018#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: GADTs, Resolution: | ScopedTypeVariables Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Ah, thank you for those examples, Simon. I was imaging GADT pattern- matching to be a sort of "whole-case" operation, but that is clearly not the case, as `f` demonstrates. So I think I'm barking up the entirely wrong tree with what I was requesting in comment:5. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12018#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: GADTs, Resolution: | ScopedTypeVariables Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I frequently find this behavior of GHC frustrating, though I fully understand why it works the way it does (and indeed don't propose a change). Perhaps the way forward is to obviate the need for such signatures by introducing visible type patterns, #11350. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12018#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: GADTs, Resolution: | ScopedTypeVariables Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13430 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * related: => #13430 Comment: See also #13430 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12018#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC