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 <[email protected]> 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 [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
