Check constructor against datatype.

[KonjacSource]

def two: Nat = suc (suc zero)

data Id : {A : U} (x y : A) -> U where
| refl : {A : U} (x : A) -> Id x x

data Exists: {A: U} {P: A -> U} -> U where
| intro: {A: U} {P: A -> U} (witness: A) (proof: P witness) -> Exists {A} {P}

def test: Exists {Nat} {Id two} = intro two (refl two)

shows

   |
10 | def exitstest: Exists {Nat} {Id two} = intro two (refl two)
   |                                                   ^
Cannot unify expected type

  ?22 two

with inferred type

  Id {Nat} two two
*** Exception: ExitSuccess

This should be ok if we check intro ... against the type Exist. But we didn't, the checking fallen to the last clause which is infer then judge equality.

[KonjacSource]

I just find this question is quite trikcy to me.
And here is my imaginary solution sofar.

With the definition, (let's just use Agda)

data Exists : {A : U} (P : A -> U) -> U where
  ex : {A : U} {P : A -> U} (a : A) → P a -> Exists P

to check ex true refl : Exists (b ≡_),

1. We notice that this is a fully applied constructor.
2. We generate metas ?A ?P ?a ?p and get Exists {?A} ?P by the signature of ex
3. We check the arguments of ex, while unifying them with ?A ?P ?a ?p

[KonjacSource]

Well, this solution failed. This is a conter-example,

data T : (n : Nat) -> U where 
| con : (m : Nat) -> T (add m m)

def test : T zero = con zero

Using the solution, it will unify T (add ?m ?m) with expected T zero. which will fail.

[KonjacSource]

I gave up, seperating parameters and indexes of data types may partially solve the problem. Let's do this later.