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]]
