Type coercion "lin X" doesn't work as expected

[heatherleaf]

The following works fine:

useVV vv =
    let vv2v : VV -> V = \vv' -> lin V vv'
    in lin VP (mkVP (vv2v vv)) ;

but this yields a type error:

 useVV vv = lin VP (mkVP (lin V vv)) ;

Here's the error message:

SecundaRulesLat.gf:
  SecundaRulesLat.gf:18:
    Happened in linearization of useVV
     no overload instance of mkVP
     for
       {act : VActForm => Str; ger : VGerund => Str; geriv : Agr => Str;
        imp : VImpForm => Str; inf : VInfForm => Str; isAux : Bool;
        part : VPartForm => Agr => Str; pass : VPassForm => Str;
        sup : VSupine => Str; lock_V : {}}
     among
       {act : VActForm => Str; ger : VGerund => Str; geriv : Agr => Str;
        imp : VImpForm => Str; inf : VInfForm => Str; lock_V : {};
        part : VPartForm => Agr => Str; pass : VPassForm => Str;
        sup : VSupine => Str}
     ...

The only thing that differs from the types is that the upper has an extra isAux:Bool, which makes it a subtype of the lower. And then it should work, as I understand things, in particular if I use lin V vv as a coercion.

The additional code is:

V = ResLat.Verb ;  -- CatLat.gf
VV = ResLat.VV ;  -- CatLat.gf
VV : Type = Verb ** { isAux : Bool } ;  -- ResLat.gf