Deriving `unsafeCoerce' using the type-nat-solver

[plaidfinch]

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 for parity 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 all n. From this, we can derive unsafeCoerce.

{-# OPTIONS_GHC -fplugin=TypeNatSolver #-}
{-# LANGUAGE DataKinds, TypeOperators, GADTs, ScopedTypeVariables, EmptyCase, TypeFamilies #-}

module Unsoundness where

import Data.Proxy
import Data.Type.Equality
import GHC.TypeLits

data Peano n where
  Z :: Peano 0
  S :: Peano n -> Peano (n + 1)

data Parity n where
  ZeroParity :: Parity 0
  OneParity  :: Parity 1

parity :: forall p n. Peano (2*n + p) -> Parity p
parity xs = walk xs xs
   where
      walk :: forall m.
              Peano (2*n -   m + p)
           -> Peano (2*n - 2*m + p)
           -> Parity p
      walk    _          Z   = ZeroParity
      walk (S _)      (S Z)  = OneParity
      walk (S ys) (S (S zs)) = walk ys zs

bad :: forall n. Peano n -> (0 :~: n)
bad n =
   case (parity :: Peano (2*x + n) -> Parity n) n of
      ZeroParity -> Refl
      OneParity  -> case (bad (S n)) of

type family IfZero n a b where
  IfZero 0 a b = a
  IfZero n a b = b

moreBad :: Peano n -> a -> Proxy b -> IfZero n a b
moreBad n a Proxy =
  case bad n of
    Refl -> a

unsafeCoerce :: forall a b. a -> b
unsafeCoerce a = moreBad (S Z) a (Proxy :: Proxy b)

[yav]

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!