Open plaidfinch opened 8 years ago
Interesting! Certainly something bogus is happening, and it is in the definition of walk
which should have been rejected. I am guessing that it has to do with the handling of -
. Here is a small example, showing just the bug:
{-# OPTIONS_GHC -fplugin=TypeNatSolver #-}
{-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies #-}
module Unsoundness where
import Data.Proxy
import Data.Type.Equality
import GHC.TypeLits
data Z n where
Z :: Z 0
test :: Proxy p -> Proxy m -> Proxy n -> Z (42 * (n - m) + p) -> p :~: 0
test _ _ _ Z = Refl
bad = test (Proxy :: Proxy 84) Proxy Proxy Z
Basically, what seems to be happening is that we don't check that the intermediate expression n - m
is not negative at the call site, but we are assuming it in the definition.
Good catch, thanks!
The following module compiles against GHC 7.10.2.
The definition of
parity
should not typecheck, but it does. In particular,p
must be constrained to the range[0,1]
in order forparity
to be type-correct, but somehow this is not enforced by the plugin. I'm not sure what's going on here.This bug allows us to derive that
0 ~ n
for alln
. From this, we can deriveunsafeCoerce
.