Type family constraints at runtime // Couldn't match type `1 <=? n0' with 'True

Question

StackOverflow!

For reasons that would like to remain between me and God, I'm currently playing around with promoting runtime naturals to the type level. I've been following this approach with GHC.TypeLits, which has worked out fine so far.

However, in one instance, I have an additional constraint of 1 <= n, i.e. my promoted natural not to be just any natural, but at least 1. This is also from GHC.TypeLits And I am unsure if/how it is possible to extract and make that information known.

Here's a minimal non-working example:

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

import Data.Maybe
import Data.Proxy
import GHC.TypeLits
import Numeric.Natural

data AnyNat (n :: Nat) where
  AN :: AnyNat n

data AtLeast1Nat (n :: Nat) where
  AL1N :: AtLeast1Nat n

promote0 :: Natural -> AnyNat n
promote0 k = case sn of
  SomeNat (_ :: Proxy p) -> AN 
  where
    sn = (fromJust . someNatVal . toInteger) k

promote1 :: (KnownNat n, 1 <= n) => Natural -> AtLeast1Nat n
promote1 k = case sn of
  SomeNat (_ :: Proxy p) -> AL1N 
  where
    sn = (fromJust . someNatVal . toInteger) k

main :: IO ()
main = do nat_in <- getLine
          let nat = read nat_in :: Natural
          let p0  = promote0 nat
          let p1  = promote1 nat
          putStrLn "Last statement must be an expression"

This produces this error (full error here, but this is the relevant part):

    * Couldn't match type `1 <=? n0' with 'True
        arising from a use of `promote1'
      The type variable `n0' is ambiguous

Honestly, this isn't too surprising and I (think I) do understand why this happens. The Natural that we give in could be any of them, so why would we be able to derive that 1 <= n? That's why it works fine for promote0 and not promote1.

My question is hence, is there any way to also check (and propagate to type-level) this information so I can use it as intended, or am I using the wrong approach here?

Answer 1

You're using the wrong approach.

As discussed in the comments, promote0 (and similarly promote1) isn't doing what you're hoping. The problem is that the AN on the right-hand-side of the case has type AnyNat n for some n entirely unrelated to the term sn. You could have written:

promote0 k = case 2+2 of 4 -> AN

and gotten much the same effect. Note the critical difference between your code and the other Stack Overflow answer you link: in that answer, the type variable n in the case scrutinee is used to type something (via ScopedTypeVariables) in the case branch. You bind a type variable p in your scrutinee but then don't use it for anything.

If we consider your actual problem, suppose we want to write something like this:

import qualified Data.Vector.Sized as V

main = do
  n <- readLn :: IO Int
  let Just v  = V.fromList (replicate n 1)
      v2 = v V.++ v
  print $ v2

This won't type check. It gives an error on V.fromList about the lack of a KnownNat constraint. The issue is that v has been assigned a type S.Vector k Int for some k :: Nat. But V.fromList performs a runtime check that the length of the input list (the run time value n) is equal to the type-level k. To do this, k must be converted to a runtime integer which requires KnownNat k.

The general solution, as you've guessed, is to construct a SomeNat that basically contains a KnownNat n => n that's unknown at compile time. However, you don't want to try to promote it to a known type-level Nat (i.e., you don't want promote0). You want to leave it as-is and case match on it at the point you need its type-level value. That type-level value will be available within the case but unavailable outside the case, so no types that depend on n can "escape" the case statement.

So, for example, you can write:

import qualified Data.Vector.Sized as V
import Data.Proxy
import GHC.TypeNats

main = do
  n <- readLn :: IO Int
  -- keep `sn` as the type-level representation of the runtime `n`
  let sn = someNatVal (fromIntegral n)
  -- scrutinize it when you need its value at type level
  case sn of
    -- bind the contained Nat to the type variable `n`
    SomeNat (Proxy :: Proxy n) -> do
      -- now it's available at the type level
      let v  = V.replicate @n 1   -- using type-level "n"
          v2 = v V.++ v
      print v2

but you can't write:

main :: IO ()
main = do
  n <- readLn :: IO Int
  let sn = someNatVal (fromIntegral n)
  let v2 = case sn of
        SomeNat (Proxy :: Proxy n) ->
          let v  = V.replicate @n 1
          in  v V.++ v
  print v2

You'll get an error that a type variable is escaping its scope. (If you want to let sized vectors leak outside the case, you need to make use of V.SomeSized or something similar.)

As for the main part of your question about handling a 1 <= n constraint, dealing with inequalities for type-level naturals is a major headache. I think you'll need to post a minimal example of exactly how you want to use this constraint in the context of a sized vector imlementation, in order to get a decent answer.