-
Notifications
You must be signed in to change notification settings - Fork 0
Open
Description
Critical
[error] -- Error: src/main/scala/typing/Typing.scala:30:27
[error] 30 | Typed[subst, Fun[Subst.Ty[subst, Var[Fresh]], t], fresh]
[error] | ^
[error] |Match type reduction failed since selector subst
[error] |matches none of the cases
[error] |
[error] | case util.HNil => typing.Var[Fresh]
[error] | case typing.Subst[typing.Var[j], t] :+: rest => typing.Var[Fresh] match {
[error] | case typing.Var[i] =>
[error] | i == j match {
[error] | case (true : Boolean) => typing.Subst.Ty[rest, t]
[error] | case Any => typing.Subst.Ty[rest, typing.Var[Fresh]]
[error] | } <: typing.Type
[error] | case typing.Fun[s, t] =>
[error] | typing.Fun[typing.Subst.Ty[subst, s], typing.Subst.Ty[subst, t]]
[error] |} <: typing.Type
Trivial
[error] -- Error: src/main/scala/lambda/DeBruijn.scala:20:28
[error] 20 | HList.Index[v, L] match {
[error] | ^
[error] | Match type reduction failed since selector (v, L)
[error] | matches none of the cases
[error] |
[error] | case (i, _) => lambda.DeBruijn.Var[i, v]
--- a/src/main/scala/lambda/DeBruijn.scala
+++ b/src/main/scala/lambda/DeBruijn.scala
@@ -18,7 +18,7 @@ object DeBruijn {
T match {
case lambda.Var[v] =>
HList.Index[v, L] match {
- case (i, _) => Var[i, v]
+ case (i, Any) => Var[i, v]
}
case lambda.Abs[v, t] => Abs[v, Transform[t, v :+: L]]
case lambda.App[t1, t2] => App[Transform[t1, L], Transform[t2, L]]
Metadata
Metadata
Assignees
Labels
No labels