Bad totality type errors

nikivazou commented 7 years ago

Totality checking is by default on, but (as with termination checking) (totality) type errors are bad. Eg

module Head where

head z = case z of
           (x:xs) -> x

 /Users/gridaphobe/Source/liquid/haskell/Head.hs:(4,1)-(5,22): Error: Liquid Type Mismatch
   Inferred type
     VV : {v : Addr# | v == "/Users/gridaphobe/Source/liquid/haskell/Head.hs:(4,10)-(5,22)|case"
                       && v == ?a}

   not a subtype of Required type
     VV : {VV : Addr# | false}

   In Context
     ?a : {?a : Addr# | ?a == "/Users/gridaphobe/Source/liquid/haskell/Head.hs:(4,10)-(5,22)|case"}

Interesting questions are

how to get better totality errors?
how do Liquid Haskell totality errors relate with GHC non-exhaustive warnings (is one subsumed by other)?
can we use GHC mechanism to get better Liquid Haskell totality errors?

gridaphobe commented 7 years ago

I forgot that we use regular liquid types to enforce the totality check, rather than the custom logic for termination checks. That does make it a bit harder to produce a nice error message.

However I think there are a couple things we can do by taking advantage of how GHC produces the runtime errors. Specifically, they pass a mangled string to the error functions, which is the value that is required to be FALSE.

"/Users/gridaphobe/Source/liquid/haskell/Head.hs:(4,10)-(5,22)|case"

I can think of two simple heuristics to improve the error messages without too much work though.

We can parse this string ourselves to report the location as (4,10)-(5,22) rather than the entire definition.
We could have a custom rule in Constraint.Generate that looks for constraints of the form {v:Addr# | v == "<path>:<loc>|case"} <: {v:Addr# | false} and emits a constraint with a custom error, using whatever mechanism we use for the termination checks.

ranjitjhala commented 7 years ago

Thanks, I meant can you add it to the README too?

The termination thing uses a special mechanism as we "know" during generation that it is a termination check.

However we can generalize your suggestion by basically extending error messages with a way to extend the error with some extra message using a regexp or some other matching. Good idea! Can you file an issue? Should be easy...

On Fri, Jul 28, 2017 at 9:33 AM Eric Seidel notifications@github.com wrote:

I forgot that we use regular liquid types to enforce the totality check, rather than the custom logic for termination checks. That does make it a bit harder to produce a nice error message.

However I think there are a couple things we can do by taking advantage of how GHC produces the runtime errors. Specifically, they pass a mangled string to the error functions, which is the value that is required to be FALSE.

"/Users/gridaphobe/Source/liquid/haskell/Head.hs:(4,10)-(5,22)|case"

I can think of two simple heuristics to improve the error messages without too much work though.

1.

We can parse this string ourselves to report the location as (4,10)-(5,22) rather than the entire definition. 2.

We could have a custom rule in Constraint.Generate that looks for constraints of the form {v:Addr# | v == ":|case"} <: {v:Addr# | false} and emits a constraint with a custom error, using whatever mechanism we use for the termination checks.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1070#issuecomment-318701486, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOAW2_yy2_aGwbHQG-sfz2dy0Rq4sks5sSg10gaJpZM4Omzcp .

ranjitjhala commented 7 years ago

Oh this is an issue .. thought it was part of the earlier PR :)

On Fri, Jul 28, 2017 at 10:43 AM Ranjit Jhala jhala@cs.ucsd.edu wrote:

Thanks, I meant can you add it to the README too?

The termination thing uses a special mechanism as we "know" during generation that it is a termination check.

However we can generalize your suggestion by basically extending error messages with a way to extend the error with some extra message using a regexp or some other matching. Good idea! Can you file an issue? Should be easy...

On Fri, Jul 28, 2017 at 9:33 AM Eric Seidel notifications@github.com wrote:

I forgot that we use regular liquid types to enforce the totality check, rather than the custom logic for termination checks. That does make it a bit harder to produce a nice error message.

However I think there are a couple things we can do by taking advantage of how GHC produces the runtime errors. Specifically, they pass a mangled string to the error functions, which is the value that is required to be FALSE.

"/Users/gridaphobe/Source/liquid/haskell/Head.hs:(4,10)-(5,22)|case"

I can think of two simple heuristics to improve the error messages without too much work though.

1.

We can parse this string ourselves to report the location as (4,10)-(5,22) rather than the entire definition. 2.

We could have a custom rule in Constraint.Generate that looks for constraints of the form {v:Addr# | v == ":|case"} <: {v:Addr# | false} and emits a constraint with a custom error, using whatever mechanism we use for the termination checks.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1070#issuecomment-318701486, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOAW2_yy2_aGwbHQG-sfz2dy0Rq4sks5sSg10gaJpZM4Omzcp .

ranjitjhala commented 7 years ago

Concretely, my proposal is simply to extend the errors with an introspection mechanism:

extraHint :: Error -> Maybe Doc

and then use extraHint before actually printing out the message.

The extraHint function could look at the actual body of the error, e.g.

Does it have the word termination or decreasing
Does it have the word Addr#

etc. and give suitable hints.

Why not just put this into the Error? We could, I suppose, but it would clutter the constraint generation logic, which should just be plain subtyping...

nikivazou commented 7 years ago

@ranjitjhala this is in the lines of how I am currently creating the termination error. The difference is that Addr# does not 1-1 map to totality checking: Addr# may appear irrespective of non-total functions.

gridaphobe commented 7 years ago

Addr# does not map 1-1 to totality checking, but I think {v:Addr# | v == "<path<:<span>"} would (or at least it's VERY close)

On Fri, Jul 28, 2017, at 10:58, Niki Vazou wrote:

@ranjitjhala this is in the lines of how I am currently creating the termination error. The difference is that Addr# does not 1-1 map to totality checking: Addr# may appear irrespective of non-total functions.

-- You are receiving this because you commented. Reply to this email directly or view it on GitHub: https://github.com/ucsd-progsys/liquidhaskell/issues/1070#issuecomment-318721874

ranjitjhala commented 7 years ago

Agree with @gridaphobe: it is almost exactly a match, plus there is also 'case' or some such that appears inside the totality errors.

On Fri, Jul 28, 2017 at 11:01 AM, Eric Seidel notifications@github.com wrote:

Addr# does not map 1-1 to totality checking, but I think {v:Addr# | v == "<path<:<span>"} would (or at least it's VERY close)

On Fri, Jul 28, 2017, at 10:58, Niki Vazou wrote:

@ranjitjhala this is in the lines of how I am currently creating the termination error. The difference is that Addr# does not 1-1 map to totality checking: Addr# may appear irrespective of non-total functions.

-- You are receiving this because you commented. Reply to this email directly or view it on GitHub: https://github.com/ucsd-progsys/liquidhaskell/issues/ 1070#issuecomment-318721874

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1070#issuecomment-318722604, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOF5Emv___0hUNemNX11Ct3JMyazxks5sSiHfgaJpZM4Omzcp .

ucsd-progsys / liquidhaskell

Bad totality type errors #1070