Closed omelkonian closed 2 months ago
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.
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).
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.
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.
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 ()
.
The interaction of levels and polymorphism pose problems, as demonstrated by the following example:
In the use site we erase the level argument completely, resulting in the wrong number of arguments when applying the polymorphic
k
function: