[GHC] #9108: GADTs and pattern type annotations?
#9108: GADTs and pattern type annotations? ------------------------------------+------------------------------------- Reporter: edsko | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- Consider {{{ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} import Data.Tagged data Sing (xs :: [k]) where SNil :: Sing '[] SCons :: SingI xs => Sing (x ': xs) class SingI (a :: [k]) where sing :: Sing a instance SingI '[] where sing = SNil instance SingI xs => SingI (x ': xs) where sing = SCons lengthSing :: forall (xs :: [k]). SingI xs => Tagged xs Int lengthSing = case sing :: Sing xs of SNil -> Tagged 0 (SCons :: Sing (x ': xs')) -> Tagged (1 + untag (lengthSing :: Tagged xs' Int)) }}} This gives a type error: {{{ Could not deduce (xs ~ (x : xs')) from the context (SingI xs) bound by the type signature for lengthSing :: SingI xs => Tagged xs Int at Bug.hs:23:15-59 ‘xs’ is a rigid type variable bound by the type signature for lengthSing :: SingI xs => Tagged xs Int at Bug.hs:23:22 Expected type: Sing xs Actual type: Sing (x : xs') }}} But once we pattern match on the `SCons` we know that `xs ~ x ': xs'` for some `x`, `xs'`, and we should be able to bring them into scope. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9108 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9108: GADTs and pattern type annotations? -------------------------------------+------------------------------------ Reporter: edsko | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by goldfire): * status: new => closed * resolution: => invalid Comment: This seems to be exactly the scenario in #6075. Essentially, GHC checks patterns from the outside working in, so it sees the type before the constructor, and before it knows about the GADT pattern match. I believe I've worked around this by doing the following painful construction: {{{ lengthSing = case sing :: Sing xs of SNil -> Tagged 0 SCons -> case sing :: Sing xs of (SCons :: Sing (x ': xs')) -> Tagged (1 + untag (lengthSing :: Tagged xs' Int)) }}} There may be a better way, but that's what I've done and it works. I suppose you could re-open as a feature request to change this behavior, if you feel so inclined. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9108#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9108: GADTs and pattern type annotations? -------------------------------------+------------------------------------ Reporter: edsko | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by edsko): Hmmmm, nasty :( I worked out in a different way, and Andres suggested yet another way (using a type family), but it seems me me that this evaluated- before-pattern-match behaviour is unfortunate behaviour; mightn't have made a difference before GADTs but with GADTs is just seems the wrong way around? Are there reasons ''not'' to evaluate the pattern match before the type annotation? (It's a tricky thing, type checking for GADTs, I realize that :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9108#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9108: GADTs and pattern type annotations? -------------------------------------+------------------------------------ Reporter: edsko | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): There is a slightly nicer encoding than Richards: {{{ lengthSing = case (sing :: Sing xs, sing) of (SNil, _) -> Tagged 0 (SCons, _ :: Sing (x ': xs')) -> Tagged (1 + untag (lengthSing :: Tagged xs' Int)) }}} We could try to make pattern signatures behave like this all the time. It's not even hard to do; I tried it and got these testsuite failures in `typecheck/` alone: {{{ Unexpected failures: should_compile T7827 [exit code non-0] (normal) should_compile tc194 [exit code non-0] (normal) should_compile tc211 [stderr mismatch] (normal) should_fail T5691 [stderr mismatch] (normal) }}} One reason is that it doesn't work for 'foralls'. Currently this works (just), and is quite convenient: {{{ f = \(x :: forall a. a -> a) -> (x True, x 'v') }}} But if you imagine applying the type signature "after the match", we'd end up unifying a forall type with a unification variable, which isn't allowed. Another thing that bugs me is that the unification that arises from a pattern signature gives rise to a coercion. What do we do with that coercion under the "match first then apply signature" story? I'm not sure what to do here. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9108#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9108: GADTs and pattern type annotations? -------------------------------------+------------------------------------ Reporter: edsko | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by edsko): Ah, that's where the catch is -- of course. That makes sense. Tricky. For the record, Andres' workaround was {{{ type family Tail (xs :: [k]) :: [k] type instance Tail (x ': xs) = xs lengthSing :: forall (xs :: [k]). SingI xs => Tagged xs Int lengthSing = case sing :: Sing xs of SNil -> Tagged 0 SCons -> Tagged (1 + untag (lengthSing :: Tagged (Tail xs) Int)) }}} which avoids a second pattern match. The fact that we need a workaround at all does seem unfortunate but I understand better now why it's required. Tricky :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9108#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC