1 2 3
File "stdin", line 4, characters 0-22: Warning: Projection value has no head constant: fun x : B => x in canonical instance a of b, ignoring it. [projection-no-head-constant,typechecker]