How can I tell GHC to satisfy a type-level <= constraint if I know it's true at runtime?

Question

I have a type parametrized by a natural number n:

data MyType (n :: Nat) = MyType

Operations on this type only make sense when n > 0, so I specified that as a constraint:

myFunction :: (KnownNat n, 1 <= n) => MyType n -> MyType n
myFunction = id

(Note that real versions of these functions do use n by turning it into a value with natVal.)

I want to create an existential type (SomeMyType) that lets us choose an n at runtime:

data SomeMyType where
  SomeMyType :: forall n. (KnownNat n, 1 <= n) => MyType n -> SomeMyType

To produce values of SomeMyType, I'm writing a someMyTypeVal function that works like someNatVal:

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
  | n > 0 = case someNatVal n of
      Just (SomeNat (_ :: p n)) -> Just (SomeMyType (MyType @n))
      Nothing                   -> Nothing
  | otherwise = Nothing

This would work perfectly fine without the 1 <= n constraint, but with the constraint I get the following type error:

• Couldn't match type ‘1 <=? n’ with ‘'True’
    arising from a use of ‘SomeMyType’

How can I get around this limitation? Since I've checked that n > 0 at runtime, I would not mind using an operation like unsafeCoerce here to convince GHC that 1 <= n is true—but I can't just use unsafeCoerce because that would lose the type-level value of n.

What's the best way of dealing with this?

Answer 1

After poking around a bit more, I found Justin L's answer to a similar question. He wrapped up his solution into the typelits-witnesses package which I was able to use to solve this problem pretty cleanly:

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n = someNatVal n >>= check
  where check :: SomeNat -> Maybe SomeMyType
        check (SomeNat (_ :: p n)) = case (SNat @1) %<=? (SNat @n) of
          LE Refl -> Just (SomeMyType (MyType @n))
          NLE _ _ -> Nothing

a %<=? b lets us compare two type-level natural numbers and gives us a witness for whether a is less than b (LE) or not (NLE). This gives us the extra constraint in the LE case to return a SomeMyType, but trying to do that in the NLE case would still give us the "can't match ‘1 <=? n’ with ‘'True’" error.

Note the explicit type signature for check—without it, the type of check is inferred as check :: SomeNat -> Maybe a and I would get the following type error:

• Couldn't match type ‘a’ with ‘SomeMyType’
   ‘a’ is untouchable
     inside the constraints: 'True ~ (1 <=? n)

With the explicit type signature everything works and the code is even (reasonably) readable.

Answer 2

As a more direct answer, the constraint 1 <= n is just a type alias for 1 <=? n ~ 'True. You can unsafely create such a type equality constraint with:

{-# LANGUAGE DataKinds, TypeOperators #-}

import Data.Type.Equality
import GHC.TypeLits
import Unsafe.Coerce

unsafeDeclarePositive :: p n -> (1 <=? n) :~: 'True
unsafeDeclarePositive _ = unsafeCoerce Refl

which is more or less what typelits-witnesses is doing under the hood.

With that definition in place, the following should type-check:

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
  | n > 0 = case someNatVal n of
      Just (SomeNat (pxy :: p n)) ->
        case unsafeDeclarePositive pxy of
          Refl -> Just (SomeMyType (MyType @n))
      Nothing -> Nothing
  | otherwise = Nothing