Blocked meta equation is not delayed but rejected

[HoshinoTented]

Code:

prim I
prim Path
variable A : Type
def infix = (a b : A) : Type => Path (\i => A) a b
def refl {a : A} : a = a => \i => a
open inductive Unit | tt
open inductive Bool | true | false
open inductive Wrap Type
| A => wrap A
// pattern matching on bool is necessary, which prevents the call from being unfolded
def someOp {T : Type} (a b : T) (bool : Bool) : Wrap T elim bool
| true => wrap a
| false => wrap b
open inductive SomeDep (T : Type) (l : T) (r : T) (b : Bool)
| con (wrap l = someOp r r b)
def what : SomeDep Unit tt tt true => con refl

Aya says:

In file <baka>:18:42 ->

  16 |   | con (wrap l = someOp r r b)
  17 |   
  18 |   def what : SomeDep Unit tt tt true => con refl
     |                                             ^--^

Error: Cannot check the expression
         refl
       of type
         (=) {Wrap ?T} (wrap ?l) (wrap ?l)
         (Normalized: wrap tt = wrap tt)
       against the type
         wrap ?l = someOp {?T} ?r ?r ?b
         (Normalized: wrap tt = wrap tt)
       In particular, we failed to unify
         wrap ?l
         (Normalized: wrap tt)
       with
         someOp {?T} ?r ?r ?b
         (Normalized: wrap tt)

[ice1000]

This is because the current impl of metas do not consider blocked evaluation. This should be delayed instead. I'll think about it.

[github-actions]

The following aya files are detected: <unnamed>.aya
Aya Version: unspecified

Exit code: 1
Output:

Compiling issue-tracker
  [Info] Resolving source file dependency
    Done in 138ms
  [Tyck] 29adb0becf6848ab868c14b115573d4d (29adb0becf6848ab868c14b115573d4d.aya)
In file 29adb0becf6848ab868c14b115573d4d.aya:16:42 ->

  14 |   open inductive SomeDep (T : Type) (l : T) (r : T) (b : Bool)
  15 |   | con (wrap l = someOp r r b)
  16 |   def what : SomeDep Unit tt tt true => con refl
     |                                             ^--^

Error: Cannot check the expression
         refl
       of type
         wrap ?l = wrap ?l
         (Normalized: wrap tt = wrap tt)
       against the type
         wrap ?l = someOp ?r ?r ?b
         (Normalized: wrap tt = wrap tt)
       In particular, we failed to unify
         wrap ?l
         (Normalized: wrap tt)
       with
         someOp ?r ?r ?b
         (Normalized: wrap tt)

I dislike the following module(s):
  29adb0becf6848ab868c14b115573d4d (29adb0becf6848ab868c14b115573d4d.aya)
Tycking interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.