How to extend ghc-typelits-natnormalise to check relationships between universally and existentially quantified types?

Question

I'm trying to make my use of Finites completely safe and non-partial, by using Proxys in place of Integers like so:

-- SO test case, re: my use of ghc-typelits-natnormalise package.
--
-- David Banas <[email protected]>
-- February 9, 2018

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

module Bogus.NewFin where

import GHC.TypeLits
import Data.Proxy
import Data.Finite
import Data.Finite.Internal (Finite(..))
import Data.Reflection

-- A safer form of `finite`.
finite' :: (KnownNat n, KnownNat m, n `CmpNat` m ~ 'GT) => Proxy m -> Finite n
finite' p = Finite $ natVal p

-- A safer form of `getFinite`.
getFinite' :: KnownNat n => Finite n -> (forall m. (KnownNat m, n `CmpNat` m ~ 'GT) => Proxy m -> r) -> r
getFinite' x f = reifyNat (getFinite x) f

And I'm getting this compiler error:

Davids-Air-2:test dbanas$ stack ghc -- -c so_natnorm.hs 

so_natnorm.hs:28:41: error:
    • Couldn't match type ‘CmpNat n n1’ with ‘'GT’
        arising from a use of ‘f’
    • In the second argument of ‘reifyNat’, namely ‘f’
      In the expression: reifyNat (getFinite x) f
      In an equation for ‘getFinite'’:
          getFinite' x f = reifyNat (getFinite x) f
    • Relevant bindings include
        f :: forall (m :: Nat).
             (KnownNat m, CmpNat n m ~ 'GT) =>
             Proxy m -> r
          (bound at so_natnorm.hs:28:14)
        x :: Finite n (bound at so_natnorm.hs:28:12)
        getFinite' :: Finite n
                      -> (forall (m :: Nat).
                          (KnownNat m, CmpNat n m ~ 'GT) =>
                          Proxy m -> r)
                      -> r
          (bound at so_natnorm.hs:28:1)

I'm guessing that my problem is trying to relate a universally and an existentially quantified type, through the mechanisms provided by the ghc-typelits-natnormalise package. Is that correct?

It seems to me that this ought to be allowed, since the caller is responsible for assigning both:

• the value of n, and
• the maximum value of m.

Where is my reasoning about this faulty?

Answer 1

reifyNat takes as an argument a function which works for any natural. A function of type forall m. (KnownNat m, n `CmpNat` m ~ 'GT) => Proxy m -> r doesn't work on any natural; it only works on naturals less than some other n.

Since you are calling getFinite to produce the actual value, you know that value is less than n. Unfortunately, you have no way to prove this to the typechecker. Fortunately, you are allowed to tell the typechecker to trust you:

import Type.Reflection ((:~:)(..))
import Unsafe.Coerce

...

getFinite'' :: KnownNat n => Finite n -> (forall m. (KnownNat m) => Proxy m -> n `CmpNat` m :~: 'GT -> r) -> r
getFinite'' x f = reifyNat (getFinite x) $ \p -> f p (unsafeCoerce Refl)

getFinite' :: forall n r . KnownNat n => Finite n -> (forall m. (KnownNat m, n `CmpNat` m ~ 'GT) => Proxy m -> r) -> r
getFinite' x f = getFinite'' x $ \p Refl -> f p