Skipping erased value arguments inside type functions in datatype parameters and in type lambdas

[viktorcsimma]

When giving type parameters to a record and using a dependent function which, however, has its value parameters erased; I've originally got an error (Kind of bound argument not supported). This PR fixes that.

The specific example (used in the test case, too):

open import Agda.Primitive

-- A record type which has both members compiled,
-- but the argument of the lambda is erased;
-- so that it won't be dependent-typed after compilation.
record Σ' {i j} (a : Set i) (b : @0 a → Set j) : Set (i ⊔ j) where
  constructor _:^:_
  field
    proj₁ : a
    proj₂ : b proj₁
open Σ' public
infixr 4 _:^:_
{-# COMPILE AGDA2HS Σ' #-}

The output here is

data Σ' a b = (:^:){proj₁ :: a, proj₂ :: b}

Update: now the arguments of type lambdas are also checked and if they are erased, they are dropped, instead of invoking an error. An example:

-- Actually, Agda can deduce here that n is erased; probably from the type signature of Σ'.
test : Nat -> Σ' Nat (λ (n : Nat) -> ⊤)
test n = n :^: tt
{-# COMPILE AGDA2HS test #-}

This produces an output like this:

test :: Natural -> Σ' Natural ()
test n = n :^: ()

[viktorcsimma]

It now seems like that it compiles, but cannot be used... I'll try to fix that.

[viktorcsimma]

Now it's OK:) I've inserted a similar check at type lambdas. See the update above.

[viktorcsimma]

One more thing apart from the comments: Type.hs has some more references to usableModality; should we change them to keepArg too? Or is there a reason why they are used there?

[jespercockx]

One more thing apart from the comments: Type.hs has some more references to usableModality; should we change them to keepArg too? Or is there a reason why they are used there?

For types it is a bit more tricky since there is the possibility of an instance argument. These can be erased at the term level, but at the type level they need to be made into a constraint. So I don't think anything there should change.