Map won't let me give an instantiation of the type it has

[robsimmons]

Truly a "Expected: ?.vector, got: ?.vector" esque error, courtesy of https://github.com/robsimmons/l10/blob/bug6/sml/splitting.sml#L67-70 (which does normal-sml-typecheck). If you can't tell, from the annotation, I played around with this one for awhile, to my increasing disbelief ;-).

CIDRE: basis construction error: 

    /Users/rjsimmon/r/l10/sml/splitting.sml:68.3-68.6 Error: 
        (map (*[ <: (Term.term_t -> t) -> Term.term_t conslist -> t conslist
         ^^^
      Sort mismatch: ('a -> 'b) -> 'a conslist -> 'b conslist & ('a -> 'b) -> 'a list -> 'b list
          expecting: (term_t -> t) -> term_t conslist -> t conslist & (term_t -> t) -> term_t list -> t list

Of course, it results from the interaction of polymorphism abstract types that turn out to be invariant.

The workaround is basically expanding the definition of map (see https://github.com/robsimmons/l10/blob/master/sml/splitting.sml#L67-68), but... seriously? That's what map is there for.

[rowandavies]

Yes, definitely a bug, you shouldn't have to do that. When in checking mode, it should always succeed if the goal is an instance of the sort scheme for the variable.

I managed to distil this one (I guess SML-CIDRE distilled is SML-Brandy?) to a small file, and basically you're just hitting the case of an intersection in the sort-scheme being instantiated while extracting upper and lower bounds for the sort variables.

Alas the two relevant parts of the CIDRE implementation make inconsistent assumptions regarding this case. One tries to "do more" and breaks the intersection in the goal sort into two separate instantiation goals. The part that solves those goals tries to "do less" and requires that the instance be the same as the goal sort aside from the variables that are instantiated.

The "do less" code is more recent so I think I just forgot to update the "do more" code. The "do less" design basically embraces sort constraints that specify the exact sort to instantiate too - so at least for now I'll follow that design.

Longer term, Rob's proposed ([[ instantiators ]]) annotation seems a fine option in this case - it's a good example of where you might want instantiators for multiple variables:

 map (*[[ term_t, t ]]*) 

Although, I'm getting tempted to just implement this to see how well it works in practice.

[rowandavies]

Fixed - both parts now follow the "do less" approach.

I also added an example based on this for instantiators annotations in "test-examples/possible-improvements".

[robsimmons]

Okay; it's still pretty silly that I have to give the conslist refinement, and even sillier that if I give

   (map (*[ <: (Term.term_t -> t) -> Term.term_t conslist -> t conslist
             & (Term.term_t -> t) -> Term.term_t list -> t list ]*)) 

instead of

   (map (*[ <: (Term.term_t -> t) -> Term.term_t list -> t list
             & (Term.term_t -> t) -> Term.term_t conslist -> t conslist ]*)) 

it gives me a type error; I guess this is related to the "do less in both cases" approach?

[rowandavies]

Yeah, that's one of the arguments for the "do more" approach. Now that I have more real examples to think about, "do more" tried to go too far by trying to account for any sequence of instantiation followed by subsorting, but "do less" may be too syntactic.

Maybe a reasonable compromise is: for each conjunct on the left you find a conjunct on the right that can be instantiated to it. Without some firmer guiding principles this seems too ad-hoc.

Separating instantiation via (*[[ ]]*) from any subsequent subsorting does seem like a better solution in terms of having firm (and obvious) guiding principles. I'll try to reconstruct the reasons why I rejected that approach, and if I can't I'll implement it as (*[[ ]]*).