Using generalized variables in function body crashes the compiler

[refparo]

open data Unit : Type | unit

open struct Wrapped (A : Type) : Type

variable B : Type

def test Unit : Wrapped B -> Unit
  | unit => \(x : Wrapped B) => unit

[ice1000]

Will implement later. I think the universe polymorphism problem is more urgent and I want to release it earlier :wink: please understand!

[lunalunaa]

New minimally reproducible example for generalized variables appearing in function result type position:

variable B : Type

public open data Unit (A : Type) : Type
| unit

def test : Unit B => unit

Here, test should have an implicit variable inserted in the telescope during resolving, but the insertion did not happen.

[ice1000]

Yay

[lunalunaa]

Yay

Please don't do anything yet. I'm fixing my gpg signature issue

[ice1000]

@lunalunaa don't forget to add a test