no overload instance for Foo among Foo

Mismatch-abstract-concrete.md

You can get this error if your abstract and concrete syntax are mismatched. Here's an example:

-- Abstract
fun NP_sleeps_S : NP -> S ;

-- Concrete
lin NP_sleeps_S np = mkS (mkCl np sleep_V) ;

Now I make a change in the abstract, but forget to update the concrete:

-- Abstract
fun NP_sleeps_Utt : NP -> Utt ;

-- Concrete
lin NP_sleeps_Utt np = mkS (mkCl np sleep_V) ;

I changed only the name in the concrete syntax, but not the right-hand side: it still starts with mkS. So I get this error:

    Happened in linearization of NP_sleeps_Utt
      no overload instance of mkS
      for
        {s : STense => Anteriority => Polarity => Order => Str;
         lock_Cl : {}}
      among
        {s : STense => Anteriority => Polarity => Order => Str;
         lock_Cl : {}}
        {s : Str; lock_Tense : {};
          t : STense} {s : STense => Anteriority => Polarity => Order => Str;
                       lock_Cl : {}}
        …
      with value type Utt

This error message is very long and verbose, so the hint "with value type Utt" is even harder to miss. But if you just squint really hard, you can see the error: no overload instance of mkS <lots of junk> with value type Utt.

(Obviously this is not easy to see, otherwise I wouldn't be writing this post.)

Now that we know what the error is, it's hard to pretend we have no idea, but in the real situation when this happens to you, it can often help to type annotate your expressions, even if you don't know if it helps. At least you might get a different error message:

-- Abstract
fun NP_sleeps_Utt : NP -> Utt ;

-- Concrete
lin NP_sleeps_Utt np = <mkS (mkCl np sleep_V) : S> ;

One thing is that once you write an explicit type annotation, "this RHS is supposed to be an S", you might notice the mismatch with the LHS, which says Utt. But suppose you don't notice it (maybe you never updated the name in the first place), let's see what is the new error message:

     Happened in linearization of NP_sleeps_Utt
      missing record fields: s type of TUseCl TPres ASimul PPos ((\s,v -> PredVP s (UseV v)) np sleep_V)
      expected: {s : Str}
      inferred: {s : CommonScand.Order => Str; lock_S : {}}

Aside from the line s type of TUseCl …, which is a bit mysterious (what is T in TUseCl?), this error message is much nicer. The compile expects a {s : Str}, but is getting (infers) some other type instead. I would personally change "inferred" to "received" or "given", because that's what it means: I wanted an Utt but you gave me an S.

The solution is just to update the concrete syntax:

-- Abstract
fun NP_sleeps_Utt : NP -> Utt ;

-- Concrete
lin NP_sleeps_Utt np = mkUtt (mkS (mkCl np sleep_V)) ;

Overloading.md

I had these two functions, preA and mkAdj:

  preA : (adj,adv : Str) -> A = \adj,adv ->
     lin A (mkAdj adj adv ** {isPre=True}) ;

  Adjective : Type = {
    s : Degr => Mod => Str ;
    isPre : Bool ;
    {- other fields, irrelevant for example -}
    } ;

  mkAdj : Str -> Str -> Adjective = \adj,adv -> {
     s = table { Positive => modTable adj ;
                 Comparative => modTable (adj + "تر") -- Regular comparative.
               } ;
     isPre = False ; {- other fields, irrelevant for example -}
  } ;

preA worked fine, until I overloaded mkAdj:

  mkAdj = overload {
    mkAdj : Str -> Str -> Adjective = \adj,adv -> { ... } ;
    mkAdj : Str -> Str -> Str -> Adjective = \pos,cmp,adv -> { ... }
  } ;

After overloading mkAdj, I got the following error message:

     Happened in operation preA
      no overload instance of mkAdj
      for
        Str Str
      among
        Str Str
        Str Str Str
      with value type {s : Degr => Mod => Str; {- other fields -} }

The last line is actually informative: with value type, where the value type is a record without isPre field. So the GF compiler thinks that mkAdj is creating something that has no isPre field at all, whereas we know that mkAdj does create an isPre field, just with the wrong value.

In other words, if you get a "no Foo among Foo", that's not the full story--"with value type Bar" is an important clue as well.

To solve the problem, you can annotate the expression with an explicit type, using the syntax <gf_expression : Type>.

preA : (adj,adv : Str) -> A = \adj,adv ->
  lin A (<mkAdj adj adv:Adjective> ** {isPre=True}) ;

Now the code works again.