メモ

Inductive eq {Ty : Set} : Ty -> Ty -> Set :=
| Refl : forall v , eq v v.

Inductive sgl {Ty : Set} : Ty -> Set :=
| Sgl : forall v , sgl v.

Definition test {ts ts' : nat} (obj : eq ts ts') (s : sgl ts) : sgl ts' :=
  match obj with
    | Refl v => s
  end.

In environment
ts : nat
ts' : nat
obj : eq ts ts'
s : sgl ts
v : nat
The term "s" has type "sgl ts" while it is expected to have type 
"sgl ?6".

一方

module hoge where

data _==_ {A : Set0} : A -> A -> Set0 where
  refl : (a : A) -> a == a

data Sgl {A : Set0} : A -> Set0 where
  sgl : (a : A) -> Sgl a

data Nat : Set0 where
  O : Nat
  S : Nat -> Nat

tinstrDenote : {ts ts' : Nat} -> (arg : ts == ts') -> Sgl ts -> Sgl ts'
tinstrDenote (refl x) s = s

この言語なら通る。ただしCoqでも

Inductive eq {Ty : Set} : Ty -> Ty -> Set :=
| Refl : forall v , eq v v.

Inductive sgl {Ty : Set} : Ty -> Set :=
| Sgl : forall v , sgl v.

Definition test {ts ts' : nat} (obj : eq ts ts') : sgl ts -> sgl ts' :=
  match obj with
    | Refl v => fun s => s
  end.

とすればいける。
あと別にこれが証明したいわけじゃなくて、最初のヤツが失敗するっていう事実を確認したかっただけです。