There is no way to explicitly provide type parameters and inference sometimes fails in reasonable contexts

[lukaszcz]

Compiling:

module check;

open import Stdlib.Data.List;
open import Stdlib.Prelude;

main : IO;
main ≔ putStrLn (natToStr (length nil));

end;

results in:

check.juvix:7:35-38: error:
Unable to infer the hole

It seems the problem is that nil can't be typed without inferring the implicit type argument. There is no mechanism yet to provide the type explicitly (at least I haven't noticed). It is conceivable that one may want to occasionally use a polymorphic constructor as an argument to a polymorphic function whose type parameter doesn't occur in the target of its type.

This also fails:

module check;

open import Stdlib.Data.List;
open import Stdlib.Prelude;

main : IO;
main ≔ putStrLn (natToStr (length (1  ∷ nil)));

end;

But this works:

module check;

open import Stdlib.Data.List;
open import Stdlib.Prelude;

inductive Unit {
  unit : Unit;
};

main : IO;
main ≔ putStrLn (natToStr (length (unit ∷ nil)));

end;

[janmasrovira]

you can provide implicit arguments using {}:

main : IO;
main ≔ putStrLn (natToStr (length (nil {Bool})));

The above should typecheck.

The second example is expected to fail as well since literals are (temporarily) given the magic type {A : Type} -> A.

[lukaszcz]

Thanks! Maybe the error message should be a bit friendlier and suggest how to provide implicit arguments? This is not used often, but once you need it you might not know what's the syntax for it (I remember having the exact same problem with Coq a long time ago when learning it).

[jonaprieto]

Please open a new issue requesting a better error message.