Non-exhaustive pattern-match warning in code-example from "Dependently Typed Programming with Singletons"
Richard Eisenberg
eir at cis.upenn.edu
Sun May 18 23:45:37 UTC 2014
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
>
More information about the ghc-devs
mailing list