Convert 'inaccessible code' errors into warnings.
AbandonedPublic

Authored by osa1 on Nov 9 2015, 9:44 AM.

Details

Summary

This fixes Trac #11066. New test case shows two functions that are operationally
same, but one of them was previously rejected by the type checker.

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Branch
t11066
Lint
Lint OK
Unit
No Unit Test Coverage
Build Status
Buildable 6594
Build 7680: GHC Patch Validation (amd64/Linux)
Build 7679: arc lint + arc unit
osa1 updated this revision to Diff 4988.Nov 9 2015, 9:44 AM
osa1 retitled this revision from to Convert 'inaccessible code' errors into warnings..
osa1 updated this object.
osa1 edited the test plan for this revision. (Show Details)
osa1 added reviewers: simonpj, rrnewton.
osa1 added a comment.Nov 9 2015, 11:13 AM

This needs more work because now it's accepting some programs that it should reject. (maybe we should just mark errors as errors rather than as warnings?)

osa1 added a comment.EditedNov 9 2015, 12:26 PM

I had a more careful look at the failures, and it seems like all of the failures are related with actually making this error a warning, which is great. (at first I thought there were some other errors that had SevWarning as severity and so those are now accepted)

But it seems like making this a warning causing CoreLint to fail!

EDIT: Lint is printing errors like:

<no location info>: warning:
    In a case alternative: (Eq# cobox_dHg :: a_awQ ~# Bool)
    cobox_axu :: () ~ Bool
    [LclId, Str=DmdType] is out of scope
<no location info>: warning:

It seems like not rejecting those programs is not enough. We need to somehow update the type checker to bind the variables mentioned in the CoreLint above, for example, and probably do some other stuff too. I'm not sure how to proceed.

osa1 added a comment.Nov 9 2015, 12:52 PM

Maybe some of the failures may be fixed by binding the variables as mentioned in my previous comment. But we have failures like this:

{-# LANGUAGE GADTs, AllowAmbiguousTypes #-}
module T8392a where

-- Should complain even with AllowAmbiguousTypes

foo :: (Int ~ Bool) => a -> a
foo x = x

This program was previously rejected because of Inaccessible code errors. Now that I made it a warning, this compiles!

Main2.hs:6:8: warning:
    Couldn't match type ‘Int’ with ‘Bool’
    Inaccessible code in
      the type signature for:
        foo :: (Int ~ Bool) => a -> a
    In the ambiguity check for the type signature for ‘foo’:
      foo :: forall a. (Int ~ Bool) => a -> a
    In the type signature for ‘foo’: foo :: (Int ~ Bool) => a -> a

Main2.hs:6:8: warning:
    Couldn't match type ‘Int’ with ‘Bool’
    Inaccessible code in
      the type signature for:
        foo :: (Int ~ Bool) => a -> a

I don't know why this was failing with an "inaccessible code" error and not some other error, but it turns out this patch is more involved.

rrnewton edited edge metadata.Nov 9 2015, 1:22 PM

For test case T8392a at least it looks like the answer is that it should in fact just be a warning, and the test suite just needs to be updated to not expect an error, right?

GHC currently doesn't bother producing valid Core when there is inaccessible code, because it expects the module not to compile, so the Core will never be looked at. Even worse, producing correct Core would be hard to do, because if Int ~ Bool is provable, type-checking is bizarre, indeed.

Instead, in inaccessible contexts, the type-checker should just replace whatever code the user wrote with some call to an error function that bleats that GHC is buggy. That certainly is more work than what you've done, but it's a lot easier than producing a correct translation of whatever funky code the user wrote!

The problem is that you learn about inaccessible code in the solver, but the Core code is actually generated during constraint generation. (It uses variables whose bindings are produced in the solver.) Perhaps the best route is to have some evidence that the code is unreachable and teach the desugarer not to look past that evidence. For example:

data G a where
  MkG :: G Bool

foo :: G Int -> String
foo x = case x of
  MkG -> "hi there!"

The type-checker would discover that "hi there!" is unreachable. The type-checker would output something like this for foo:

foo :: G Int -> String
foo x = case x of
  MkG -> let ev1 = UNREACHABLE in "hi there!"

When the desugarer is converting this to Core, it would see the UNREACHABLE and do this:

foo :: G Int -> String
foo = \x -> case x of
  MkG -> error "unreachable code"

Even better would be to manufacture some evidence of unreachability and put that in the Core code. (Two examples of unreachability evidence are a coercion that Int ~ Bool and a coercion that a ~ [a].) CoreLint could then be taught about unreachability. But that's probably a research-grade project.

@simonpj, any thoughts here?

rrnewton added a comment.EditedNov 9 2015, 2:02 PM

If the silly/impossible constraints are purely local (and on code that's never executed), what's the problem with type-checking those expressions assuming, e.g., Int ~ Bool?

If the silly/impossible constraints are purely local (and on code that's never executed), what's the problem with type-checking those expressions assuming, e.g., Int ~ Bool?

It's just that the solver can't cope with that assumption. I suppose it could just drop the assumption, but then the user would get spurious type errors. For example:

data G2 a where
  MkG2Char :: G2 Char
  MkG2Bool :: G2 Bool

foo :: G2 a -> a
foo g@MkG2Char = case g of
  MkG2Bool -> not 'x'

I think that's actually type-correct. But there's no way the solver can figure that out. Perhaps we could improve the solver to do so, but that's surely a waste of time. And it's not helpful to issue an error about not being applied to a character there. So I think it's much better not to bother trying to produce correct Core in this instance but just bail.

Ok. I was just trying to understand what "can't cope with" means.

If it's replaced with error I guess that's fine but it means you get no type checking whatsoever in those branches right? But you get the warning....

Ok. I was just trying to understand what "can't cope with" means.

If it's replaced with error I guess that's fine but it means you get no type checking whatsoever in those branches right? But you get the warning....

That's right. You get no type checking whatsoever in inaccessible code. But I actually think that's the correct behavior. From a logical standpoint, those branches have an assumption of False. So anything should be considered well-typed, by ex falso quodlibet.

bgamari requested changes to this revision.Nov 11 2015, 4:52 AM
bgamari edited edge metadata.

@osa1, do you think you could update this to produce the error'ing Core that @goldfire suggested?

This revision now requires changes to proceed.Nov 11 2015, 4:52 AM
osa1 added a comment.Nov 11 2015, 7:23 AM

Yes, but not before the weekend I'm afraid.

In D1454#42495, @osa1 wrote:

Yes, but not before the weekend I'm afraid.

Any progress on this?

osa1 added a comment.Nov 27 2015, 8:38 AM

I made some progress but it needs some more work... Will keep working on this.

What's left on this one? Is it going to make the GHC 8.0 feature freeze? (Which... doesn't seem to have an exact hour and minute atm?)

simonpj edited edge metadata.Dec 14 2015, 7:30 AM

There was muttering about Lint errors. Last comment from osa was "will work on this". I can try to help if needed.

S

osa1 added a comment.EditedDec 14 2015, 7:35 AM

Hi all,

I was very busy with first UnboxedSums patch and then with finals(last week of the semester), and I won't have any time for this until Friday. If anyone wants to take over this patch please go ahead, I don't want to block others.

Since it's clear by now that UnboxedSums won't make it to 8.0 I think I can focus on this one.

I'd like to see this. Here's a slight variant on @goldfire's suggestion for implementation:

  1. Add a new form of evidence to Core, which takes a coercion between two "obviously apart" types (e.g. Int ~ Bool) and produces an arbitrary type. This wouldn't be terribly dissimilar from how -fdefer-type-errors works.
  2. When there are "unreachable code" warnings, i.e. insoluble givens, use this new form of evidence to bind all the unsolved/insoluble wanteds.

This would mean we waste time typechecking inaccessible code, but I doubt that's such a big deal.

One wrinkle is that a ~ [a] is not, strictly speaking, unreachable in Core. Defining type family X where X = [X] we obtain a solution, although GHC will typically loop forever rather than finding it. Thus "obviously apart" includes distinct type constructors but not occurs check failures. I guess in such a situation we could report an inaccessibility warning and otherwise typecheck normally.

@osa1, what is the status of this?

osa1 added a comment.Dec 20 2016, 10:29 PM

@bgamari I don't have enough time these days unfortunately. If anyone's interested please don't wait for me to complete this patch. If no one shows up I'll try to give this another try next week.

austin resigned from this revision.Nov 6 2017, 10:16 PM
RyanGlScott abandoned this revision.Jun 3 2018, 6:40 AM
RyanGlScott added a subscriber: RyanGlScott.

This approach was abandoned in favor of D4744.