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]