MissingTyVar works

Author: bladyjoker

experimental/prolog/lb-compiler/kind_check.pl

@@ -122,13 +122,8 @@
 ctx(ctx(ModuleName, TyName, _Sol, Args), arg(TyVar),K) :-
     print_message(informational, ctx(arg(TyVar.var_name.name), ModuleName-TyName-K)),
     (
-        first(_{
-                  arg_name: _{name: TyVar.var_name.name, source_info: _},
-                  arg_kind: K
-              },
-              Args
-             ) -> true;
-        throw(error(missing_ty_var(ModuleName, TyName,TyVar,Args)))
+        find_arg(Args, TyVar, K) -> true;
+        throw(error(missing_ty_var(ModuleName, TyName, TyVar, Args)))
     ).
 
 ctx(ctx(ModuleName, TyName, Sol, _Args), ref(TyRef), K) :-
@@ -147,6 +142,10 @@
         throw(error(missing_ty_ref(ModuleName, TyName, TyRef, Sol)))
     ).
 
+find_arg([Arg|Args], TyVar, K) :-
+    Arg.arg_name.name = TyVar.var_name.name -> K = Arg.arg_kind;
+    find_arg(Args, TyVar, K).
+
 find_sol([Mn-Tn-K_|Sol], ModuleName, TyName, K) :-
     pretty_module_name(ModuleName, ModuleName_),
     pretty_module_name(Mn, Mn_),
@@ -179,7 +178,8 @@
                 KArg=TyArg.arg_kind
             ),
             KArgs),
-    kind_check_ty(ctx(Mn, Tn, Rs, [TyArg|As]), TyBody, KBody),
+    append(TyArgs, As, As_),
+    kind_check_ty(ctx(Mn, Tn, Rs, As_), TyBody, KBody),
     kind_arrow_(KArgs, KBody, K).
 
 kind_check_ty(_Ctx, '.lambdabuffers.compiler.TyBody'{opaque: _}, K) :-
@@ -405,12 +405,12 @@
     ty_local_ref_("Int", IntTyRef),
     ty_def_opaque("String", StringTyDef),
     ty_local_ref_("String", StringTyRef),
-    ty_var("f", TyVarF1),
-    ty_app(TyVarF1, [IntTyRef, StringTyRef], TyApp),
+    ty_var("f", TyVarF),
+    ty_app(TyVarF, [IntTyRef, StringTyRef], TyApp),
     ntuple([TyApp], MkAProd),
     constr("MkA", MkAProd, MkAConstr),
     sum([MkAConstr], FooTyBody),
-    ty_arg("f1", KF1, TyArg),
+    ty_arg("f", KF, TyArg),
     ty_abs([TyArg], FooTyBody, FooAbs),
     ty_def_abs("Foo", FooAbs, FooTyDef),
     mod("Mod", [FooTyDef, StringTyDef, IntTyDef], Mod),
@@ -437,6 +437,20 @@
                         "ModBar"-"Bar"-(*)
                     ]).
 
+test("\nmodule Mod\nsum Foo a = MkA b", [ ]) :-
+    ty_var("b", TyVarB),
+    ntuple([TyVarB], MkAProd), constr("MkA", MkAProd, MkAConstr),
+    sum([MkAConstr], FooTyBody),
+    kind_ref(type, KStar),
+    ty_arg("a", KStar, TyArgA),
+    ty_abs([TyArgA], FooTyBody, FooAbs),
+    ty_def_abs("Foo", FooAbs, FooTyDef),
+    mod("Mod", [FooTyDef], Mod),
+    comp_input([Mod], CompIn),
+    catch(
+        kind_check(CompIn, _Solution),
+        error(missing_ty_var(_, _, TyV, _)),
+        TyV.var_name.name = "b").
 
 :- end_tests(kind_check).
 
@@ -461,6 +475,13 @@
         ]
     ].
 
+prolog:message(missing_ty_var(ModuleName, TyName, TyVar, _Args))
+--> {pretty_module_name(ModuleName, Mn)},[
+        'Error while kind checking type ~w.~w: Missing type variable ~w '-[
+            Mn, TyName.name, TyVar.var_name.name
+        ]
+    ].
+
 prolog:message(ctx(Q, ModuleName-TyName-Kind))
 --> { pretty_module_name(ModuleName, Mn), pretty_kind(Kind, K) },
         ['Context ~w.~w :: ~w was queried with ~w'-[