QuantifiedConstraints Weirdness

fails.hs

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
​
module Test where
​
import Protolude
​
import Control.Monad.Random (Random(..), getRandom)
​
-------------------------------------------------------------------------------
-- Fields
-------------------------------------------------------------------------------
​
class (Num k, Random k) => Field k
​
newtype Prime (p :: Nat) = F {toInt :: Integer} deriving Show
​
instance KnownNat p => Num (Prime p) where
  F x + F y     = F (rem (x + y) (natVal (witness :: Prime p)))
  F x * F y     = F (rem (x * y) (natVal (witness :: Prime p)))
  F x - F y     = F (rem (x - y) (natVal (witness :: Prime p)))
  fromInteger x = F (mod x (natVal (witness :: Prime p)))
  abs           = panic "not implemented."
  signum        = panic "not implemented."
​
instance KnownNat p => Random (Prime p) where
  random  = first F . randomR (0, natVal (witness :: Prime p) - 1)
  randomR = panic "not implemented."
​
instance KnownNat p => Field (Prime p)
​
-------------------------------------------------------------------------------
-- Curves
-------------------------------------------------------------------------------
​
data Point f q r = Point q q q deriving Show
​
class (forall p . (KnownNat p, r ~ Prime p), Field q, Field r) => Curve f q r where
  gen :: Point f q r -- Curve generator
  mul :: Point f q r -> Prime p -> Point f q r -- Bad multiplication
  mul = (. toInt) . mul'
  mul' :: Point f q r -> Integer -> Point f q r -- Good multiplication
  mul' p n
    | n == 0    = Point 0 1 0
    | n == 1    = p
    | even n    = p'
    | otherwise = add p p'
    where
      p'
        = mul' (add p p) (div n 2)
      add (Point x y z) (Point x' y' z')
        = Point (x + x') (y + y') (z + z')
​
instance Curve f q r => Random (Point f q r) where
  random  = first (mul gen) . random
  randomR = panic "not implemented."
​
class Curve A q r => ACurve q r where
  genA :: Point A q r
​
instance (Field q, Field r, ACurve q r) => Curve A q r where
  gen = genA
​
-------------------------------------------------------------------------------
-- Example
-------------------------------------------------------------------------------
​
data A
​
type Fq = Prime 0xb0000000000000000000000953000000000000000000001f9d7
​
type Fr = Prime 0xb0000000000000000000000953000000000000000000001f9d7
​
instance ACurve Fq Fr where
  genA = Point
    0x101efb35fd1963c4871a2d17edaafa7e249807f58f8705126c6
    0x22389a3954375834304ba1d509a97de6c07148ea7f5951b20e7
    1
​
main :: IO ()
main = (getRandom :: IO (Point A Fq Fr)) >>= print

succeeds.hs

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
​
module Test where
​
import Protolude
​
import Control.Monad.Random (Random(..), getRandom)
​
-------------------------------------------------------------------------------
-- Fields
-------------------------------------------------------------------------------
​
class (Num k, Random k) => Field k
​
newtype Prime p = F {toInt :: Integer} deriving Show
​
instance Num (Prime p) where
  F x + F y     = F (x + y)
  F x * F y     = F (x * y)
  F x - F y     = F (x - y)
  fromInteger x = F x
  abs           = panic "not implemented."
  signum        = panic "not implemented."
​
instance Random (Prime p) where
  random  = first F . random --(0, natVal (witness :: Prime p) - 1)
  randomR = panic "not implemented."
​
instance Field (Prime p)
​
-------------------------------------------------------------------------------
-- Curves
-------------------------------------------------------------------------------
​
data Point f q r = Point q q q deriving Show
​
class (forall p . r ~ Prime p, Field q, Field r) => Curve f q r where
  gen :: Point f q r -- Curve generator
  mul :: Point f q r -> Prime p -> Point f q r -- Bad multiplication
  mul = (. toInt) . mul'
  mul' :: Point f q r -> Integer -> Point f q r -- Good multiplication
  mul' p n
    | n == 0    = Point 0 1 0
    | n == 1    = p
    | even n    = p'
    | otherwise = add p p'
    where
      p'
        = mul' (add p p) (div n 2)
      add (Point x y z) (Point x' y' z')
        = Point (x + x') (y + y') (z + z')
​
instance Curve f q r => Random (Point f q r) where
  random  = first (mul gen) . random
  randomR = panic "not implemented."
​
class Curve A q r => ACurve q r where
  genA :: Point A q r
​
instance (Field q, Field r, ACurve q r) => Curve A q r where
  gen = genA
​
-------------------------------------------------------------------------------
-- Example
-------------------------------------------------------------------------------
​
data A
​
type Fq = Prime ()--0xb0000000000000000000000953000000000000000000001f9d7
​
type Fr = Prime ()--0xb0000000000000000000000953000000000000000000001f9d7
​
instance ACurve Fq Fr where
  genA = Point
    0x101efb35fd1963c4871a2d17edaafa7e249807f58f8705126c6
    0x22389a3954375834304ba1d509a97de6c07148ea7f5951b20e7
    1
​
main :: IO ()
main = (getRandom :: IO (Point A Fq Fr)) >>= print