Opened 4 years ago

Closed 3 years ago

#11518 closed bug (fixed)

Test TcCoercibleFail hangs with substitution sanity checks enabled

Reported by: niteria Owned by: niteria
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.1
Keywords: Cc: simonpj, goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time performance bug Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

When working on https://phabricator.haskell.org/D1862 I've run into an issue where TcCoercibleFail test would hang and eventually timeout.

To move forward I've disabled the check for applyTysX in Type, by changing substTyWith to substTyWithUnchecked.

To reproduce:

  1. change substTyWithUnchecked back to substTyWith in applyTysX
  2. in testsuite: make TEST=TcCoercibleFail, the test will hang

What I've established so far:

The calls to substTy become slower and slower with stack traces like this:

CallStack (from ImplicitParams):
  pprSTrace, called at compiler/types/TyCoRep.hs:1903:35 in ghc:TyCoRep
  checkValidSubst, called at compiler/types/TyCoRep.hs:1943:17 in ghc:TyCoRep
  substTy, called at compiler/types/TyCoRep.hs:1796:23 in ghc:TyCoRep
  substTyWith, called at compiler/types/Type.hs:1429:15 in ghc:Type
  applyTysX, called at compiler/types/Coercion.hs:1261:11 in ghc:Coercion
  instNewTyCon_maybe, called at compiler/types/Coercion.hs:1308:23 in ghc:Coercion
  unwrapNewTypeStepper, called at compiler/typecheck/FamInst.hs:278:9 in ghc:FamInst
  unwrap_newtype, called at compiler/typecheck/FamInst.hs:265:15 in ghc:FamInst
  ()

substTy is called with exponentially growing substitution types of the form (), ((),()), (((),()),((),()))... : https://phabricator.haskell.org/P88 (warning: big file). If you look at the test file it's easy to see how such types could arise.

Change History (22)

comment:1 Changed 4 years ago by Bartosz Nitka <niteria@…>

Blocking: 11371 removed

comment:2 Changed 4 years ago by niteria

Blocking: 11371 added

comment:3 Changed 4 years ago by niteria

Owner: set to niteria

I'm going to dig more, but I expect I might not know how to best fix this. In general how does the typechecker deal with types that can get exponential?

The part of the code that generates such types is:

newtype VoidBad a = VoidBad (VoidBad (a,a))

comment:4 Changed 4 years ago by thomie

Blocking: 11371 removed

comment:5 Changed 4 years ago by simonpj

OK. If the reason that the ASSERT gets exponentially expensive is that the types get exponentially large, that's a good explanation. That indeed is a hard problem (see e.g. #9198).

But what's odd is that it doesn't bomb out on us when the ASSERT is not there. That seems odd to me -- if the types get very large I'd expect the type checker to fail even in the absence of the ASSERT.

comment:6 Changed 4 years ago by niteria

But what's odd is that it doesn't bomb out on us when the ASSERT is not there. That seems odd to me -- if the types get very large I'd expect the type checker to fail even in the absence of the ASSERT.

I think I can explain this. The unwrapNewTypeStepper is protected by a checkRecTc which will cause an abort if the same newtype constructor is unwrapped 100 times. The difference I believe is due to laziness and sharing, it's easy to create an exponentially big type by repeated substitution into (a, a) and unless a is (deeply) forced at some point you can do it in sub-exponential time. So when substTy began to force it by computing the free variables for the sanity check the problem became visible.

In other words the recursion check in checkRecTc didn't need to force the type to decide it was a loop, so it wasn't bothered by it growing exponentially (made possible by sharing and laziness) before.

comment:7 Changed 4 years ago by simonpj

OK, but even with the new ASSERT, checkRecTc will cut off the recursion and so will not unwrap the newtype 100 times. So where is the big type coming from? I'm still missing that.

comment:8 Changed 4 years ago by niteria

If you unwrap it 100 times you end up with a type that has size 2^100. Computing free vars of such type would take forever. And the ASSERT in substTy does exactly that. It's enough to unwrap it 30 times for it to become unbearably slow.

That type is very regular and a very compact representation because of sharing. The type is essentially:

a0 = ()
a1 = (a0, a0) -- note the sharing, but when free vars are 
              -- computed they are computed for fst and snd independently
a2 = (a1, a1)
a3 = (a2, a2)

a100 = (a99, a99) -- this has size 2^100, O(2^n) when naively explored, 
                  -- but it's represented as a sequence of O(n) pointers.

comment:9 Changed 4 years ago by simonpj

But the question is: why doesn't checkRecTc cut off the unwrapping? That's what you seemed to say in comment:6

comment:10 Changed 4 years ago by goldfire

And why is it checking for unwrapping 100 times? I thought checkRecTc stopped at 2, not 100. Was there a reason to increase it? Maybe we've gone too far.

Nice analysis, by the way.

comment:11 Changed 4 years ago by niteria

It's always been 100: [0b7e538a09bc958474ec704063eaa08836e9270e].

why doesn't checkRecTc cut off the unwrapping?

It *does* (or would if we run it long enough), but 100 is way too big in case of a type that's growing exponentially.

comment:12 in reply to:  11 Changed 4 years ago by goldfire

Replying to niteria:

It's always been 100: [0b7e538a09bc958474ec704063eaa08836e9270e].

No. Before that commit, checkRecTc allowed one unwrapping. The second failed (because the TyCon was in the NameSet nearby. But there's also a reference to the ticket that inspired the increase, which is helpful.

I guess, in the end, we're never going to get this number correct. We could just have a flag for it, as suggested in the code there. Then, for this test, we use the flag.

In the end, we're talking about a slowdown that affect only DEBUG compilers, yes? So I'm more worried about getting the test to pass before the end of the universe than in actually removing the exponential behavior -- especially given that the user's program indeed introduces the exponential behavior.

comment:13 Changed 4 years ago by niteria

What are the next steps here? I can make it a flag and use it to make the test pass.

comment:14 Changed 4 years ago by simonpj

I don't know. I still don't understand WHY this assert is causing exponential behaviour in this example and I'm reluctant to suppress it until we know.

In typecheck/should_fail/TcCoercibleFail I see

newtype Fix f = Fix (f (Fix f))
foo6 = coerce :: Fix (Either Int) -> Fix (Either Age)
foo7 = coerce :: Fix (Either Int) -> ()

which is presumably the cause of the problem? But that looks nothing like the example in comment:8. Nor can I see where 100-level unwrappping would happen. So I'm lost.

Fortunately it doesn't affect a normal stage-2 validate.

comment:15 Changed 4 years ago by niteria

No, I don't think the example from comment:14 is related.

We have

newtype VoidBad a = VoidBad (VoidBad (a,a))
foo5' = coerce :: (VoidBad ()) -> ()

For coerce :: (VoidBad ()) -> () to typecheck we have to know if VoidBad () and () have the same runtime representation. So we need to find out what VoidBad () really is. So we start unwrapping the newtypes of off it.

What do we get when we try to unwrap the newtype off of VoidBad ()?

VoidBad () = VoidBad ((),())
= VoidBad (((),()),((),()))
= VoidBad ((((),()),((),())),(((),()),((),())))
= ...

It's clear that the type we apply to VoidBad grows exponentially and that VoidBad () diverges. Before adding the ASSERT this is detected by checkRecTc. The reason that checkRecTc manages to do that in the presence of an exponentially growing argument to VoidBad is that checkRecTc only counts how many times we've applied VoidBad. It never looks at the exponentially growing argument.

The reason why we are able to build an exponentially growing arguments with small amount of space and time has to do with sharing. When we apply VoidBad a = VoidBad (a, a) it is the *same* a that goes to the left and right component of the pair. The a is shared between both components.

The way we apply VoidBad a = VoidBad (a, a) is by using the substTy function. We replace every a from the right hand side with a from the left hand side. But in this case we use the *same* a, so the size of the type grows exponentially, but the representation doesn't.

The problem arises when substTy examines the argument we passed as a to look for the free vars to do the ASSERT. Since the type grows exponentially, the time to compute the free vars also grows exponentially and we don't get to the 100th iteration of unwrapping in any reasonable amount of time.

comment:16 Changed 4 years ago by simonpj

Aha. I was looking in the wrong place. Good explanation.

I've added a comment to the test to flag this up.

Now I understand, and we've documented that understanding, I'm happy to close this.

Simon

comment:17 Changed 4 years ago by goldfire

Before we close this, don't we still need to add the flag? Or maybe break out that part of TcCoercibleFail into a new test that is disabled in DEBUG mode?

comment:18 Changed 4 years ago by Simon Peyton Jones <simonpj@…>

In a96c4e7/ghc:

Add comments to TcCoercibleFail

Flag up the problem highlighted in Trac #11518 comment:15

comment:19 Changed 4 years ago by goldfire

I just tripped over this, with TcCoercibleFail timing out when testing against a DEBUG build. Can we somehow tell the testsuite to skip this one in this scenario until we have a better workaround?

comment:20 in reply to:  19 Changed 4 years ago by thomie

Replying to goldfire:

Can we somehow tell the testsuite to skip this one in this scenario until we have a better workaround?

Add the following setup function to the test definition in all.T:

when(compiler_debugged(), skip)

I made that change in 49c55e68aae9841c166430ae566b0d9bdc03c99d. You might need a git pull.

comment:21 Changed 4 years ago by goldfire

@thomie: Great -- thanks!

comment:22 Changed 3 years ago by niteria

Resolution: fixed
Status: newclosed

I think we've done all we could here.

Note: See TracTickets for help on using tickets.