Haskellで型レベルプログラミング(あるいはごく簡単な証明)を書くときに, DataKindsでデータ型をそのまま持ち上げると困る場面がある. {-# LANGUAGE DataKinds, GADTs, TypeOperators, TypeFamilies #-} data a :=: b where Refl :: a :=: a data Nat = Zero…