Non-exhaustive pattern-match warning in code-example from "Dependently Typed Programming with Singletons"

[Richard Eisenberg]

A little more tinkering got this working, with the definitions in my earlier email, below (with ScopedTypeVariables):

index :: forall i n t. (i :<? S n) => 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 <eir at cis.upenn.edu> 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 :<? n2 where
>>  ltProof :: n1 :< n2
>> 
>> type family LTSupport n1 n2 where
>>  LTSupport Z     n     = (() :: Constraint)
>>  LTSupport (S m) (S n) = m :<? n
>> 
>> instance Z :<? (S n) where
>>  ltProof = LTZ
>> 
>> instance (m :<? n) => (S m) :<? (S n) where
>>  ltProof = LTS ltProof
>> 
>> index :: (i :<? l) => 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 <hvriedel at gmail.com> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>