Opened 4 years ago

Last modified 11 months ago

#11243 new feature request

Flag to not expand type families

Reported by: crockeea Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler Version: 7.10.2
Keywords: TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Error messages can be ugly, especially when working with promoted types. I've been dealing with this for a long time with [one library in particular](https://hackage.haskell.org/package/lol). But I just encountered something truly heinous. Due to a minor mistake, GHC spit out 8 errors in total, the shortest of which was 60 lines, and the longest of which was 20,046 lines long. That's no typo: the last error is over 20,000 lines long. Props to GHC for handling such a mess. As the library author, I've learned to look paste these massive errors. But I'm afraid that some user is going to have a heart attack (or worse: give up and go home).

You can see in the error message that most of it is recurring blocks of

PrimePower
('PP
  '(type-natural-0.3.0.0:Data.Type.Natural.Definitions.SSym1
      (type-natural-0.3.0.0:Data.Type.Natural.Definitions.SSym1
         (type-natural-0.3.0.0:Data.Type.Natural.Definitions.SSym1
            (type-natural-0.3.0.0:Data.Type.Natural.Definitions.SSym1
               (type-natural-0.3.0.0:Data.Type.Natural.Definitions.SSym1
                  (type-natural-0.3.0.0:Data.Type.Natural.Definitions.SSym1
                     (type-natural-0.3.0.0:Data.Type.Natural.Definitions.SSym1
                        type-natural-0.3.0.0:Data.Type.Natural.Definitions.ZSym0)))))),
    type-natural-0.3.0.0:Data.Type.Natural.Definitions.SSym1
      type-natural-0.3.0.0:Data.Type.Natural.Definitions.ZSym0))

and

(NextListElt
  *
  zq
  ((':)
     *
     (ZqBasic * Types.Q18869761 Types.Z)
     ((':)
        *
        (Types.Zq * Types.Q19393921, ZQ1)
        ((':)
           *
           (Types.Zq * Types.Q19918081, ZQ2)
           ((':)
              *
              (Types.Zq * Types.Q2149056001, ZQ3)
              ((':)
                 *
                 (Types.Zq * Types.Q3144961, ZQ4)
                 ((':)
                    * (Types.Zq * Types.Q7338241, ZQ5) ('[] *))))))))),

I believe that GHC attempts to expand type synonyms as much as possible, which is great in many cases. But for this error, the repetition of fully expanded blocks completely hides the true nature of the error, especially since the user (obviously) makes heavy use of type synonyms anyway.

The feature I'm requesting is the ability to somehow reduce the mess in the attached error. Here are a few ideas:

  1. A flag to tell GHC to *not* expand type synonyms, i.e. if the user uses N2 from Data.Type.Natural, GHC should print 'N2' instead of
    type-natural-0.3.0.0:Data.Type.Natural.Definitions.SSym1
     (type-natural-0.3.0.0:Data.Type.Natural.Definitions.SSym1
       type-natural-0.3.0.0:Data.Type.Natural.Definitions.ZSym0)
    
  2. Allow library developers a way to tell the compiler how to print a certain entity, i.e., with a custom name. This is somewhat similar to the Custom Type Errors proposal, but I don't think that proposal includes a way to tell GHC how to print specific types/type synonyms.

Has anyone else run into this issue before? Are there any existing solutions or other ideas?

Attachments (1)

ghcierror.zip (58.4 KB) - added by crockeea 4 years ago.
Zip of error file

Download all attachments as: .zip

Change History (19)

comment:1 Changed 4 years ago by crockeea

Apparently, this error is too big for Trac and for LPaste. So you'll just have to take my word for it.

comment:2 Changed 4 years ago by rwbarton

Well, it might help to have some idea of the structure of the error message at least.

Have you tried with HEAD? I think there have been changes in when type synonyms are expanded in error messages.

Changed 4 years ago by crockeea

Attachment: ghcierror.zip added

Zip of error file

comment:3 Changed 4 years ago by crockeea

I was able to compress the error and attach it. Unfortunately, I don't have an easy way to test with HEAD. The test was with 7.10.2.

comment:4 Changed 4 years ago by rwbarton

So the large types appear in the known constraints and the types of things in scope, like

examples/Main.hs:113:23:
    Could not deduce (Typeable (* -> *) sym0)
      arising from a use of ‘genKeys’
    from the context [LARGE]
      bound by the inferred type of
               prfTest :: [LARGE]
      at examples/Main.hs:(104,1)-(123,18)
    The type variable ‘sym0’ is ambiguous
    Relevant bindings include
      ast0 :: [LARGE]
        (bound at examples/Main.hs:110:3)
    In the first argument of ‘evalCryptoRandIO’, namely
      ‘(genKeys v ast0)’
    In the second argument of ‘(=<<)’, namely
      ‘evalCryptoRandIO (genKeys v ast0)’
    In a stmt of a 'do' block:
      (ast1, idMap) <- time "Generating keys: "
                       =<< evalCryptoRandIO (genKeys v ast0)

I think this isn't what changed in HEAD; that was when the error actually involved a disagreement between types which were expressed using type synonyms.

comment:5 Changed 4 years ago by simonpj

I believe that GHC attempts to expand type synonyms as much as possible

On the contrary, GHC tries not to expand type synonyms unless necessary.

So the first thing to do is to look at a small example, and see why it is failing to not-expand them. Can you make a test case that is as small as possible, in which a type synoym is expanded that you'd rather wasn't? (I.e. NOT one that demonstrates (as above) that unnecessary expansion is undesirable; we all believe that already.)

It's possible that there's a good reason. Then the next thing is to think whether we could improve GHC's existing techniques for delaying expansion.

Finally you could try to re-compress expanded types, though that sounds harder.

Definitely a good project!

comment:6 Changed 4 years ago by goldfire

Just to clarify what may be an auxiliary issue: GHC has made a (arbitrary) decision that vanilla type synonyms (type Foo = ...) should not be expanded, while type families should be expanded. The idea is that type families do computation and it might be useful to see the results of computation. This decision could be revisited or usefully controlled by a flag.

Also, we're a bit hamstrung when it comes to expanding constraint synonyms, which tend to get expanded quite eagerly. But it's hard to do better. Is this what you're seeing?

comment:7 Changed 4 years ago by crockeea

I believe both of the major replicated blocks are due to type families. The PrimePower block is due to singletons, which makes heavy use of type families. Ideally, it would say something more like PrimePower (PP (N7, N1)). The NextListElt block also comes from a type family: while the type list itself is a simple type synonym, NextListElt is a type family. In that case, I'd like to see NextListElt * zq MyTypeList.

comment:8 Changed 4 years ago by goldfire

Ah, so I think we've solved it then. Your experience is by design. And it's a design we settled on based on a different bug report asking for the opposite behavior of what you want. (I don't recall the ticket number.)

Time to introduce -fno-print-expanded-type-families?

comment:9 Changed 4 years ago by crockeea

Summary: Use Type Synonyms to Compress ErrorsFlag to not expand type families

Please! That would (likely) solve the issue reported in this ticket.

I can't find a ticket where the solution was to expand type families, perhaps someone else recalls the reason for that choice? I wonder if a more granular approach might be warranted. Perhaps we could say -fno-print-expanded-type-families -fprint-tf NextListElt to *only* expand NextListElt? I don't have a concrete use case for this off the top of my head, but if some people want TFs to be expanded, it seems like there should be some sort of intermediate solution.

comment:10 Changed 4 years ago by goldfire

The Right Solution is to be more like Idris and allow users to, say, click on parts of error messages to expand or contract them. That's a major project. But the pressure is mounting for such an improvement, and so I'll leery of putting in gobs more complexity into command-line flags.

comment:11 Changed 4 years ago by crockeea

Sounds like a good long-term solution, and in the short term -fno-print-expanded-type-families should suffice.

comment:12 Changed 4 years ago by simonpj

The underlying issue is this:

  • Suppose F is a type function with an instance for F [Int]. If we have constraints
    1. (C (F [Int])), where C is a class
    2. F [Int] ~ Maybe Bool
    3. G (F [Int]) ~ Maybe Bool then we want to apply the instance in case that unlocks the class constraint or equality.
  • That expansion may be fruitless. For (1), perhaps F [Int] expands to Bool, C has no Bool instance. Then would you prefer to see "can't solve C (F [Int])" or "can't solve C Bool? Perhaps the latter.
  • In (3) we might expand F [Int] vigorously to get a big type, and still not be able to simplify the call to G.

In the case of type synonyms we can have the best of both worlds. Say we have

type T a = S a a

Then the type T [Int] is represented (essentially) as a pair of its expanded and un-expanded form; so we can freely choose to use either at any time.

But it's not so easy for type functions becuase the expanded and un-expanded forms are not interchangeable; there's a coercion involved.

I think we could still be a bit less aggressive about expansion. We even implemted this once. But we disabled it for ill-understood performance reasons. Here is the Note from TcFlatten:

Note [Lazy flattening]
~~~~~~~~~~~~~~~~~~~~~~
The idea of FM_Avoid mode is to flatten less aggressively.  If we have
       a ~ [F Int]
there seems to be no great merit in lifting out (F Int).  But if it was
       a ~ [G a Int]
then we *do* want to lift it out, in case (G a Int) reduces to Bool, say,
which gets rid of the occurs-check problem.  (For the flat_top Bool, see
comments above and at call sites.)

HOWEVER, the lazy flattening actually seems to make type inference go
*slower*, not faster.  perf/compiler/T3064 is a case in point; it gets
*dramatically* worse with FM_Avoid.  I think it may be because
floating the types out means we normalise them, and that often makes
them smaller and perhaps allows more re-use of previously solved
goals.  But to be honest I'm not absolutely certain, so I am leaving
FM_Avoid in the code base.  What I'm removing is the unique place
where it is *used*, namely in TcCanonical.canEqTyVar.

See also Note [Conservative unification check] in TcUnify, which gives
other examples where lazy flattening caused problems.

Bottom line: FM_Avoid is unused for now (Nov 14).
Note: T5321Fun got faster when I disabled FM_Avoid
      T5837 did too, but it's pathalogical anyway

In short, here's a project for someone!

comment:13 Changed 4 years ago by goldfire

Simon is right. I was thinking of the case in #10321, which is much simpler, as it concerns only output in GHCi. The behavior you're observing does not seem like it will easily succumb to controlling with a flag.

comment:14 Changed 4 years ago by thomie

Keywords: TypeFamilies added

comment:15 Changed 3 years ago by bgamari

Milestone: 8.2.18.4.1

It doesn't look like this will happen for 8.2.

comment:16 Changed 22 months ago by bgamari

Milestone: 8.4.18.6.1

This ticket won't be resolved in 8.4; remilestoning for 8.6. Do holler if you are affected by this or would otherwise like to work on it.

comment:17 Changed 17 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be fixed for 8.6, bumping to 8.8.

comment:18 Changed 11 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

Note: See TracTickets for help on using tickets.