fork download

copy

{-# LANGUAGE RankNTypes   #-}
{-# LANGUAGE TypeFamilies #-}
 
module Phantom where
 
data Zero
data Succ n
 
type One   = Succ  Zero
type Two   = Succ  One
type Four  = Succ (Succ Two )
type Six   = Succ (Succ Four)
type Eight = Succ (Succ Six )
 
class Nat n where
    toInt :: n -> Int
instance Nat Zero where
    toInt _ = 0
instance (Nat n) => Nat (Succ n) where
    toInt _ = 1 + toInt (undefined :: n)
 
newtype Pointer n = MkPointer Int
newtype Offset  n = MkOffset  Int
 
multiple :: forall n. (Nat n) => Int -> Offset n
multiple i = MkOffset (i * toInt (undefined :: n))
 
add :: Pointer m -> Offset n -> Pointer (GCD Zero m n)
add (MkPointer x) (MkOffset y) = MkPointer (x + y)
 
fetch32 :: (GCD Zero n Four ~ Four) => Pointer n -> IO ()
fetch32 = undefined
 
type family   GCD  d        m        n
type instance GCD  d        Zero     Zero    = d
type instance GCD  d       (Succ m) (Succ n) = GCD (Succ d) m n
type instance GCD  Zero    (Succ m)  Zero    = Succ m
type instance GCD (Succ d) (Succ m)  Zero    = GCD One d m
type instance GCD  Zero     Zero    (Succ n) = Succ n
type instance GCD (Succ d)  Zero    (Succ n) = GCD One d n

[1 of 1] Compiling Phantom          ( prog.hs, prog.o )

prog.hs:20:19: error:
    • Could not deduce (Nat n1) arising from a use of ‘toInt’
      from the context: Nat n
        bound by the instance declaration at prog.hs:19:10-32
      The type variable ‘n1’ is ambiguous
      These potential instances exist:
        instance Nat n => Nat (Succ n) -- Defined at prog.hs:19:10
        instance Nat Zero -- Defined at prog.hs:17:10
    • In the second argument of ‘(+)’, namely ‘toInt (undefined :: n)’
      In the expression: 1 + toInt (undefined :: n)
      In an equation for ‘toInt’: toInt _ = 1 + toInt (undefined :: n)
   |
20 |     toInt _ = 1 + toInt (undefined :: n)
   |                   ^^^^^^^^^^^^^^^^^^^^^^

prog.hs:26:28: error:
    • Could not deduce (Nat n0) arising from a use of ‘toInt’
      from the context: Nat n
        bound by the type signature for:
                   multiple :: forall n. Nat n => Int -> Offset n
        at prog.hs:25:1-48
      The type variable ‘n0’ is ambiguous
      These potential instances exist:
        instance Nat n => Nat (Succ n) -- Defined at prog.hs:19:10
        instance Nat Zero -- Defined at prog.hs:17:10
    • In the second argument of ‘(*)’, namely ‘toInt (undefined :: n)’
      In the first argument of ‘MkOffset’, namely
        ‘(i * toInt (undefined :: n))’
      In the expression: MkOffset (i * toInt (undefined :: n))
   |
26 | multiple i = MkOffset (i * toInt (undefined :: n))
   |                            ^^^^^^^^^^^^^^^^^^^^^^

Standard output is empty