Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Deriving `unsafeCoerce' using the type-nat-solver #7

Open
kwf opened this issue Jan 19, 2016 · 1 comment

Comments

@kwf
Copy link

commented Jan 19, 2016

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

This comment has been minimized.

Copy link
Owner

commented Jan 20, 2016

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!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants
You can’t perform that action at this time.