Opened 4 years ago

Closed 4 years ago

Last modified 4 years ago

#9108 closed bug (invalid)

GADTs and pattern type annotations?

Reported by: edsko Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.8.2
Keywords: 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

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.

Change History (4)

comment:1 Changed 4 years ago by goldfire

Resolution: invalid
Status: newclosed

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.

comment:2 Changed 4 years ago 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 :)

comment:3 Changed 4 years ago 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

comment:4 Changed 4 years ago 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 :)

Note: See TracTickets for help on using tickets.