#15057 closed bug (fixed)

Lint types created by newFamInst

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.4.1
Keywords: TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #15012 Differential Rev(s): Phab:D4611
Wiki Page:

Description

In #15012, we observed a terrible failure resulting from newFamInst creating a type family instance with an unbound type variable on the right-hand side. What's worse, -dcore-lint didn't catch it! Let's fix that by calling lintType on the types involved in newFamInst.

A wrinkle in this plan is that lintType currently expands all type synonyms, but the offending type in #15012 had the unbound variable occur in a type synonym application, so expanding type synonyms would make this naughtiness seemingly vanish (from Core Lint's perspective). We should configure lintType so that one can control its type synonym expansion behavior.

Change History (9)

comment:1 Changed 19 months ago by RyanGlScott

Differential Rev(s): Phab:D4611
Status: newpatch

comment:2 Changed 19 months ago by Ben Gamari <ben@…>

In 257c13d8/ghc:

Lint types in newFamInst

We weren't linting the types used in `newFamInst`, which
might have been why #15012 went undiscovered for so long. Let's fix
that.

One has to be surprisingly careful with expanding type synonyms in
`lintType`, since in the offending program (simplified):

```lang=haskell
type FakeOut a = Int

type family TF a
type instance TF Int = FakeOut a
```

If one expands type synonyms, then `FakeOut a` will expand to
`Int`, which masks the issue (that `a` is unbound). I added an
extra Lint flag to configure whether type synonyms should be
expanded or not in Lint, and disabled this when calling `lintTypes`
from `newFamInst`.

As evidence that this works, I ran it on the offending program
from #15012, and voilà:

```
$ ghc3/inplace/bin/ghc-stage2 Bug.hs -dcore-lint
[1 of 1] Compiling Foo              ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.5.20180417 for x86_64-unknown-linux):
        Core Lint error
  <no location info>: warning:
      In the type ‘... (Rec0 (FakeOut b_a1Qt))))’
      @ b_a1Qt is out of scope
```

Test Plan: make test TEST=T15057

Reviewers: simonpj, goldfire, bgamari

Reviewed By: bgamari

Subscribers: thomie, carter

GHC Trac Issues: #15057

Differential Revision: https://phabricator.haskell.org/D4611

comment:3 Changed 19 months ago by bgamari

Resolution: fixed
Status: patchclosed

comment:4 Changed 19 months ago by simonpj

Thanks for doing this, but I don't think it's quite right yet.

As you have it, we

  • Expand type synonyms usually
  • But not when calling from newFamInst

But that isn't what we want. Consider these definitions:

type S1 x = Int
type S2 x = x Int

In regular Core, if a is not in scope, it'd be bad to have a type S1 a. Likewise S2 (Int Int) would be bad (kind error). With your patch this will be missed.

Moreover, in newFamInst, it's ok to have a RHS with a partially-applied type synonym like S2 S1. But I think your patch will reject it.

What we want is something like this:

  • In a type-synonym application S t1 .. tn:
    1. Expand the synonym and lint the result
    2. But also lint t1..tn independently, to find any out-of-scope variables or kind errors

The trouble is that in t1..tn we are allowed to have an un-saturated synonym application, but only at top level. For example, suppose Then S2 S1 is fine, but S2 (Maybe S1) is not. Of course, the latter is detected in step (1). But it won't be detected in S1 (Maybe S1). I think I don't care about that; un-saturated synonyms in a phantom argument.

So that would make the rule be as follows:

  • Have a flag report-unsat-syns
  • In a type-synonym application S t1 .. tn:
    1. If report-unsat-syns is on, and S has arity more than n, report an unsaturated synonym
    2. If report-unsat-syns is on, expand the synonym and lint the result
    3. Regardless of report-unsat-syns, lint t1..tn independently with report-unsat-syns off, to find any out-of-scope variables or kind errors
  • Switch on report-unsat-syns for the arguments of AppTy and TyConApp with non-synonym type constructor.

There is some duplicated work here: for non-phantom arguments, if report-unsat-syns is on, all the work of (3) is done by (2). So you could do (3) only for phantom arguments.

comment:5 Changed 19 months ago by simonpj

Resolution: fixed
Status: closednew

comment:6 Changed 19 months ago by RyanGlScott

What you propose sounds fine. But I'm not going to be working on it, as I've already exceeded my time budget for this.

comment:7 Changed 19 months ago by simonpj

Fair enough. But meanwhile perhaps we can revert the patch, since it adds complexity but does not achieve the goal.

comment:8 Changed 19 months ago by Simon Peyton Jones <simonpj@…>

In 6da5b87/ghc:

Better linting for types

Trac #15057 described deficiencies in the linting for types
involving type synonyms.  This patch fixes an earlier attempt.

The moving parts are desrcribed in
  Note [Linting type synonym applications]

Not a big deal.

comment:9 Changed 19 months ago by simonpj

Resolution: fixed
Status: newclosed
Note: See TracTickets for help on using tickets.