[Agda] Re: Simple DepType Pattern Matching

[Yuya Uezato]

Hi Wouter.

Thank you for answer.

I learnt "dot patterns" for first time.

> f : Ty unit -> Unit
> f (ty .unit) = unit

This passed type-checking.

I think that "dot patterns" is effective for repeated variable ,and making effective restriction/constraints from type signature.

But,there are things that has not understood yet. 

1.Why must use a indirect method?
<<code>>
f : (Th unit) -> Unit
f (th unit) = unit
<<code>>
It seems to be correct...

2.Question about Agda2 type-checking internal
<<code>>
data Unit : Set0 where
  unit : Unit

data Th : Unit -> Set0 where
  th : (u : Unit) -> Th u

f : (Th unit) -> Unit
f (th unit) = unit -- not "dot patterns" on purpose
{-
u != unit of type Unit
when checking that the pattern th unit has type Th unit
-}

g : (Th unit) -> Unit
g (th nons) = unit
{-
nons != unit of type Unit
when checking that the pattern th nons has type Th unit
-}
<<code>>
function f's error message have "u != unit" but function g's error message have "nons != unit".

These messages are strange for me.
Probably "u" of "u != unit" is "u : A" of type-signature of data-constructor "th".
However, why do it(= "u") appear in such a place?

Thanks for your help.

--
Yuya