Proving properties of type-level natural numbers obtained from user input

[Bas van Dijk]

Hi,

I have another type-level programming related question:

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE ScopedTypeVariables #-}
> {-# LANGUAGE KindSignatures #-}
>
> import GHC.TypeLits

Say I have a Proxy p of some type-level natural number:

> p :: forall (n :: Nat). Proxy n
> p = Proxy

Imagine I get p from user input like this:

> main :: IO ()
> main = do
>     [arg] <- getArgs
>     let n = read arg :: Integer
>
>     case someNatVal n of
>       Nothing -> error "Input is not a natural number!"
>       Just (SomeNat (p :: Proxy n)) -> ...

I also have a function f which takes a proxy of a natural number but
it has the additional constraint that the number should be lesser than
or equal to 255:

> f :: forall (n :: Nat). (n <= 255) => proxy n -> ()
> f _ = ()

How do I apply f to p?

Obviously, applying it directly gives the type error:

> f p
<interactive>:179:1:
    Couldn't match expected type ‘'True’ with actual type ‘n0 <=? 255’
    The type variable ‘n0’ is ambiguous
    In the expression: f p
    In an equation for ‘it’: it = f p

I imagine I somehow need to construct some Proof object using a function g like:

> g :: forall (n :: Nat). proxy n -> Proof
> g _ = ...

Where the Proof constructor encapsulates the (n <= 255) constraint:

> data Proof where
>     NoProof :: Proof
>     Proof :: forall (n :: Nat). (n <= 255)
>           => Proxy n -> Proof

With g in hand I can construct c which patterns matches on g p and
when there's a Proof the (n <= 255) constraint will be in scope which
allows applying f to p:

> c :: ()
> c = case g p of
>       NoProof -> error "Input is bigger than 255!"
>       Proof p -> f p

But how do I define g?

Cheers,

Bas