Misleading error when using lincat as parameter

[daherb]

When loading the following Grammar

abstract TestAbs = {
  cat
    Temp ; Pol ; Cl ; S ; 
  fun
    UseCl  : Temp -> Pol -> Cl -> S ;
}

  param Order   = Ord | Subord | Quest;
  lincat
    Cl = {s : Temp => Bool => Order => Str};
    S = {s : Order => Str};
    Pol = {s : Str ; b : Bool};
    Temp = { t : Bool * Bool } ;
  lin
    UseCl temp pol cl = { --Temp -> Pol -> Cl -> S ;  
      s = \\o => case o of {
	Ord => cl.s ! lin Temp temp ! pol.b ! Ord;
	_ => "Baz" 
	};
      };
}

this error occurs
compiling Test.gf... src/compiler/GF/Compile/GeneratePMCFG.hs:(430,42)-(431,76): Non-exhaustive patterns in case

[Thomas-H]

The example can be reduced a little bit more:

abstract TestAbs = {
  cat
    Temp ; Cl ; S ; 
  fun
    UseCl  : Temp -> Cl -> S ;
}

concrete Test of TestAbs = {
  param Pol = Pos;
  lincat
    Cl = {s : Temp => Str};
    S = {s : Str};
    Temp = { t : Pol } ;
  lin
    UseCl temp cl = { s = cl.s ! lin Temp temp; };
}

The root of the problem seems to be the use of the lincat Temp as an index in a table, Temp => Str }. Show this even be allowed?

It's the lock fields that are added to lincats that cause problem when you use lincats in this way. They cause problems in GeneratePMCFG in two ways actually:

• There is an assumption that the record fields are in sorted order, but it appears that the lock fields break that assumption, in this example creating a mismatch between {t=…,lock_Temp=…} and {lock_Temp=…,t=…} and causing a lookup to fail.
• If you write just temp instead of lin Temp temp there will be a mismatch between {t=…} and {lock_Temp=…,t=…}, again causing a lookup to fail (and you also get a warning about the missing lock field lock_Temp at an earlier stage).

As a quick fix, maybe it's enough to add some code in GeneratePMCFG to discard the lock fields before doing the lookup that currently fails, but perhaps there is a better place to fix this… @krangelov ?

[inariksit]

I stumbled upon a similar bug a while ago, but figured that it's such a marginal use case to use lincats in weird ways that I didn't bother to report :-P For curiosity, here it is (sorry it's not even a self-contained example, it was from NounAra.gf):

-- Relevant definitions
Agr = NounPer3 {g:Gender ; n:Number} | Pron PerGenNum ; 
PN = {s : Case => Str; g : Gender; n : Number} ;
NP = {s : Case => Str ; a = Agr} ;

-- Bug appears here
UsePN pn = {
    s = pn.s;
    a = NounPer3 pn -- this causes internal error in GeneratePMCFG
--    a = NounPer3 {g=pn.g ; n=pn.n} -- this works
    } ;

[Thomas-H]

Hmm, maybe it is not only lock fields that can cause problems, maybe record subtyping in general can cause problems, in this case a mismatch between records {s,g,n} and {g,n}. Maybe a more elaborate fix is needed…

[krangelov]

Indeed, the problem is in the type checker which is in a very shaky state. It works for the most common cases but fails as soon as you try something unconventional. Sub-typing is only one of the things that it doesn't handle well. Honestly it needs to be replaced completely. I had started this a while ago but I never got the time and energy to complete it.

…

On Tue, 12 Feb 2019 at 15:12, Thomas H ***@***.***> wrote: Hmm, maybe it is not only lock fields that can cause problems, maybe record subtyping in general can cause problems, in this case a mismatch between records {s,g,n} and {g,n}. Maybe a more elaborate fix is needed… — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#35 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ATBZZPWgYN70emYj50W6Qb_c5oHGRPK4ks5vMsvkgaJpZM4a2CVV> .

[heatherleaf]

Aren't you discussing two different problems here? In Krasimir's example the problem is record subtyping ({s,g,n} vs {g,n}). But in Herbert's and Thomas' examples, the problem is using an abstract category as a linearisation type.

Here's a version of Thomas' example that compiles:

concrete Test of TestAbs = {
param Pol = Pos;
lincat
  Cl = {s : {t : Pol} => Str}; -- writing Temp instead of {t:Pol} throws "Non-exhaustive patterns in case"
  S = {s : Str};
  Temp = {t : Pol};
lin
  UseCl temp cl = {s = cl.s ! temp};
}

(Perhaps both are symptoms of the same bug of course)