Nonexhaustive patternmatch warning in codeexample from "Dependently Typed Programming with Singletons"
Herbert Valerio Riedel
hvriedel at gmail.com
Sun May 18 15:54:42 UTC 2014
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 nonexhaustive
 In an equation for ‘index’: Patterns not matched: Nil _
`
So I would have expected to workaround that by explicitly wrapping the
lengthphantom with the promoted `S` typeconstructor, 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 patternmatch warning, I now
get a typechecking 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
nonexhaustive patternmatch?
Cheers,
HVR
[1]: http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf
More information about the ghcdevs
mailing list