A little more tinkering got this working, with the definitions in my earlier email, below (with ScopedTypeVariables): index :: forall i n t. (i : List (S n) t -> SNat i -> t index (x :- _) SZ = x index (_ :- xs) (SS (i :: SNat i')) = case ltProof :: i' :< n of LTZ -> index xs i LTS _ -> index xs i I offer no technique that can generalize this process, though... Richard On May 18, 2014, at 7:45 PM, Richard Eisenberg wrote:

The short answer here (to "Is there a way to avoid the non-exhaustive pattern-match warning?") is "no, not in general". See #3927 (https://ghc.haskell.org/trac/ghc/ticket/3927).

And, after some playing around, I couldn't find a way to do this in your specific example, either. I will say that I've found that GHC sometimes has more luck with constructions like this (over Boolean-valued type families):

...

data n1 :< n2 where LTZ :: Z :< (S n) LTS :: m :< n -> (S m) :< (S n)

class LTSupport n1 n2 => n1 :

type family LTSupport n1 n2 where LTSupport Z n = (() :: Constraint) LTSupport (S m) (S n) = m :

instance Z :

instance (m : (S m) :

index :: (i : List l t -> SNat i -> t index (x :- _) SZ = x index (_ :- xs) (SS i) = index xs i

But, that didn't help your particular problem.

This is precisely why `singletons` exports the `bugInGHC` function. When I write code like yours, I include

...

index _ _ = bugInGHC

as the last line of `index`. This suppresses the warning but is painful. I always do make sure that GHC indeed rejects non-wildcard patterns before doing this, but it would be great if we didn't have to do it at all!

Richard

On May 18, 2014, at 11:54 AM, Herbert Valerio Riedel wrote:

...

Hello *,

I've been experimenting with the code from the "Dependently Typed Programming with Singletons" paper[1] from the following is derived (modulo some irrelevant renamings):

{-# LANGUAGE TypeOperators, DataKinds, GADTs, TypeFamilies #-}

module CheckedList where

data Nat = Z | S Nat

data SNat n where SZ :: SNat Z SS :: SNat n -> SNat (S n)

infixr 5 :- data List l t where Nil :: List Z t (:-) :: t -> List l t -> List (S l) t

type family n1 :< n2 where m :< Z = False Z :< (S m) = True (S n) :< (S m) = n :< m

index :: (i :< l) ~ True => List l t -> SNat i -> t index (x :- _) SZ = x index (_ :- xs) (SS i) = index xs i

The problem, though, is that with the code above GHC 7.8.2 emits a warning for the `index` function:

,---- | Pattern match(es) are non-exhaustive | In an equation for ‘index’: Patterns not matched: Nil _ `----

So I would have expected to workaround that by explicitly wrapping the length-phantom with the promoted `S` type-constructor, like so

index :: (i :< S l) ~ True => List (S l) t -> SNat i -> t index (x :- _) SZ = x index (_ :- xs) (SS i) = index xs i

While this would probably have silenced the pattern-match warning, I now get a type-checking error I can't seem to get rid of:

,---- | Could not deduce (l1 ~ 'S l0) from the context ((i :< 'S l) ~ 'True) | bound by the type signature for | index :: (i :< 'S l) ~ 'True => List ('S l) t -> SNat i -> t | | or from ('S l ~ 'S l1) | bound by a pattern with constructor | :- :: forall t (l :: Nat). t -> List l t -> List ('S l) t, | in an equation for ‘index’ | | or from (i ~ 'S n) | bound by a pattern with constructor | SS :: forall (n :: Nat). SNat n -> SNat ('S n), | in an equation for ‘index’ | | ‘l1’ is a rigid type variable bound by | a pattern with constructor | :- :: forall t (l :: Nat). t -> List l t -> List ('S l) t, | in an equation for ‘index’ | | Expected type: List ('S l0) t | Actual type: List l1 t | Relevant bindings include | xs :: List l1 t | | In the first argument of ‘index’, namely ‘xs’ | In the expression: index xs i `----

Is there a way to tweak the code so that GHC doesn't think there's a non-exhaustive pattern-match?

Cheers, HVR

[1]: http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs