Levels should not always be erased

[omelkonian]

The interaction of levels and polymorphism pose problems, as demonstrated by the following example:

open import Haskell.Prelude
open import Agda.Primitive using (lzero)

k : a → b → a
k x _ = x
{-# COMPILE AGDA2HS k #-}

testK : Nat
testK = k 42 lzero
{-# COMPILE AGDA2HS testK #-}

In the use site we erase the level argument completely, resulting in the wrong number of arguments when applying the polymorphic k function:

import Numeric.Natural (Natural)

k :: a -> b -> a
k x _ = x

testK :: Natural
testK = k 42

    • Couldn't match expected type ‘Natural’
                  with actual type ‘b0 -> a0’
    • Probable cause: ‘k’ is applied to too few arguments
      In the expression: k 42
      In an equation for ‘testK’: testK = k 42
  |
9 | testK = k 42
  |         ^^^^

[flupe]

Very interesting edge case!

What would be the proper way to prevent this though?
Should agda2hs replace it with () when given to specialized polymorphic functions? Parametricity ought to mean it's fine. But I have no idea how to reliably check this. In particular because it would still fail with partial applications:

open import Haskell.Prelude
open import Agda.Primitive using (lzero)

k : a → b → a
k x _ = x
{-# COMPILE AGDA2HS k #-}

l : Level → Nat
l = k 42
{-# COMPILE AGDA2HS l #-}

testK : Nat
testK = l lzero
{-# COMPILE AGDA2HS testK #-}

Which would yield:

import Numeric.Natural (Natural)

k :: a -> b -> a
k x _ = x

l :: Natural
l = k 42

testK :: Natural
testK = l

Seems to me like the only proper fix would be to always compile Level to () but that's a bit sad.

[jespercockx]

I believe the proper fix here is to decide which arguments to drop based on the uninstantiated type of the function, i.e. when compiling a list of arguments we should decide which arguments to erase based on the type of the function but not on the values of the (previous) arguments. In this case we would then get to actually compiling the lzero term, which should throw an error (since there is no level type in Haskell).

[flupe]

But if you look at the example I posted with a partial application of a polymorphic function, the term lzero is an argument to a function whose argument type has already been unified with Level. And this function is completely fine and does not use levels at all. So I don't think this check would be enough.

[jespercockx]

Oh you are correct, it would still be a problem. Thinking about it a bit more, the real problem is that the type parameter is instantiated to Level, which shouldn't be allowed because Level is not a Haskell type. So we could fix it perhaps by checking that (non-erased) type arguments are actually valid Haskell types before dropping them.

[jespercockx]

More careful checking of type parameters reveals an issue in our Prelude implementation: the guard function in Haskell.Control.Monad has the following signature:

guard : {{ MonadFail m }} → (b : Bool) → m (b ≡ True)

However b ≡ True is not a valid Haskell type! With the check, this causes problems when guard is used in a larger expression, e.g. guard ... >> .... To fix this, we should change the type of guard to

guard : {{ MonadFail m }} → (b : Bool) → m (Erase (b ≡ True))

so its type compiles to the proper MonadFail m => Bool -> m ().