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

[Richard Eisenberg]

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
>