haskell-jp / questions #101 at 2022-07-23 22:29:56 +0900

nobsun
2022-07-23 22:29:56 +0900
の練習問題3.2の証明をで書こうとして絶賛はまり中。
というか、エラーメッセージが理解できないでいます。`Could no deduce: If (x == x) t ('Var x) ~ t` なぜなんでしょう？
```src/Gmachine/AExprLet.hs:245:24: error:
• Could not deduce: If (x == x) t ('Var x) ~ t
from the context: s ~ 'Var x1
bound by a pattern with constructor:
SVar :: forall (x :: Name). Sing x -> Sing ('Var x),
in a case alternative
at src/Gmachine/AExprLet.hs:244:5-11
or from: x1 ~ x
bound by a pattern with constructor:
Refl :: forall {k} (a :: k). a :~: a,
in a case alternative
at src/Gmachine/AExprLet.hs:245:16-19
Expected: Sing (Substitute s x t)
Actual: Sing t
't' is a rigid type variable bound by
the type signature for:
saSubstitute :: forall (s :: AExpr) (x :: Name) (t :: AExpr).
Sing s -> Sing x -> Sing t -> Sing (Substitute s x t)
at src/Gmachine/AExprLet.hs:239:1-101
• In the expression: st
In a case alternative: Proved Refl -> st
In the expression:
case sx %~ sy of
Proved Refl -> st
Disproved _ -> ss
• Relevant bindings include
st :: Sing t (bound at src/Gmachine/AExprLet.hs:240:20)
sx :: Sing x (bound at src/Gmachine/AExprLet.hs:240:17)
saSubstitute :: Sing s
-> Sing x -> Sing t -> Sing (Substitute s x t)
(bound at src/Gmachine/AExprLet.hs:240:1)
|
245 | Proved Refl -> st
| ^^```
mod_poppo
2022-07-24 10:02:56 +0900
抽象的な型変数 x に対しては x == x から True への簡約は行われません。 https://hackage.haskell.org/package/base-4.16.2.0/docs/Data-Type-Equality.html#t:-61--61- の定義を見ると、規則 a == a = True が発動するのは x が「何らかの型コンストラクタ f に対して f a と書くことができない」ことが既知の場合のみで、抽象的な型変数に対してはそれはわからないのです。型の等価性演算子を独自に
type family a === b where
  a === a = True
  a === b = False

という風に定義するか、 Substitute の定義を書き換えて == を使わないようにすれば解決すると思います。
nobsun
2022-07-24 21:40:29 +0900
ありがとうございます。Twitter で @mr_konnさんにも同様にアドバイス https://twitter.com/mr_konn/status/1550864037071572992
https://twitter.com/mr_konn/status/1550862653144252417
をいただきました。 Substitution の定義の書き換えを試みていますが、理解がおいついていなくて、うまく定義しきれていません。