search

zydeco-lang / zydeco

a proof-of-concept programming language based on Call-by-push-value
Other
49 stars 3 forks source link

Better Type Error Messages #42

Open maxsnew opened 1 year ago

maxsnew commented 1 year ago
  1. The current type error messages are panics, which we should never raise unless there is a bug in zydeco
  2. The error messages themselves are not that informative: "thread 'main' panicked at 'called Result::unwrap() on an Err value: KindMismatch { context: "desugaring type application", expected: CType, found: VType }', zydeco-lang/src/zydeco.rs:60:50"
LighghtEeloo commented 1 year ago

Oops, wrong reference above. Addressed in f58f62ea789315cdc2979524bd1876e631791347. The trace of type checking is now printed after the error site, and the unwraps are removed.

maxsnew commented 11 months ago

Got this message: 

Error: In resolve codata, expected type application, but got forall (A : VType) . Thunk(Mo(A)) -> Thunk(A -> Compu) -> Compu
    (cbpv.zy:149:7 - 149:25)

What does in resolve codata mean? Can we give it a more descriptive message?

LighghtEeloo commented 11 months ago

The text after in ... is supposed to tell us which process of type-checking we are in. In the current implementation, resolve_[data/codata] is the function that handles type applications and type name resolution on nominal data / codata types, given that nominal types have weird equalities and we don't yet have a fresh or abstract type in the core calculus. Given this cursed implementation, I guess the idea of "letting the user know which part the type checker is working on" doesn't make much sense anymore, at least not in resolve codata.

I'm changing the header of the message, i.e. the context, to one of the following:

  1. In codata resolution,
  2. In (the context of) determining the type of a codata definition that requires some type arguments,

Or, potentially, I can turn the whole sentence around: "We got \ during \ but \ is required."

I can also rework on the type checker to support fresh type in the core calculus.

LighghtEeloo commented 11 months ago

A quick attempt that I'd like to patch for now, but if that's still not satisfactory, I'll definitely improve.