Opened 7 years ago

Last modified 23 months ago

#4296 new bug

The dreaded SkolemOccurs problem

Reported by: simonpj Owned by: simonpj
Priority: low Milestone:
Component: Compiler Version: 6.12.3
Keywords: Cc: dimitris@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_compile/Simple20
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

The "SkolemOccurs" problem is a celebrated difficulty with combining (a) termination and (b) completeness, in this example:

type instance F [a] = [F a]
f :: (F [a] ~ a) => ...

Currently we err on the side of completeness, and lose termination:

Simple20.hs:9:1:
    Context reduction stack overflow; size = 21
    Use -fcontext-stack=N to increase stack size to N
      co :: F [F (F (F (F (F (F (F (F (F (F a)))))))))]
              ~
            F (F (F (F (F (F (F (F (F (F a)))))))))
      co :: F (F (F (F (F (F (F (F (F a))))))))
              ~
            [F (F (F (F (F (F (F (F (F (F a)))))))))]
      co :: F [F (F (F (F (F (F (F (F (F a))))))))]
              ~
            F (F (F (F (F (F (F (F (F a))))))))
      co :: F (F (F (F (F (F (F (F a)))))))
              ~
            [F (F (F (F (F (F (F (F (F a))))))))]
      co :: F [F (F (F (F (F (F (F (F a)))))))]
              ~
            F (F (F (F (F (F (F (F a)))))))
      co :: F (F (F (F (F (F (F a))))))
              ~
            [F (F (F (F (F (F (F (F a)))))))]
      co :: F [F (F (F (F (F (F (F a))))))] ~ F (F (F (F (F (F (F a))))))
      co :: F (F (F (F (F (F a))))) ~ [F (F (F (F (F (F (F a))))))]
      co :: F [F (F (F (F (F (F a)))))] ~ F (F (F (F (F (F a)))))
      co :: F (F (F (F (F a)))) ~ [F (F (F (F (F (F a)))))]
      co :: F [F (F (F (F (F a))))] ~ F (F (F (F (F a))))
      co :: F (F (F (F a))) ~ [F (F (F (F (F a))))]
      co :: F [F (F (F (F a)))] ~ F (F (F (F a)))
      co :: F (F (F a)) ~ [F (F (F (F a)))]
      co :: F [F (F (F a))] ~ F (F (F a))
      co :: F (F a) ~ [F (F (F a))]
      co :: F [F (F a)] ~ F (F a)
      co :: F a ~ [F (F a)]
      co :: F [F a] ~ F a
      co :: a ~ [F a]
      co :: F [a] ~ a

Change History (13)

comment:1 Changed 7 years ago by simonpj

Description: modified (diff)

comment:2 Changed 7 years ago by simonpj

See also indexed-types/should_compile/Simple13, which compiles ok.

comment:3 Changed 7 years ago by igloo

Milestone: 7.2.1
Owner: set to simonpj

comment:4 Changed 6 years ago by simonpj

See also indexed_types/should_fail/SkolemOccursLoop which takes a long time. Daniel says "Without limiting the heap, my 4G of RAM don't even agree with a context- stack of 30 for SkolemOccursLoop. And stage2 didn't react to ^C or kill -TERM, so it had to be kill -KILLed."

comment:5 Changed 6 years ago by simonpj

I reduced the context stack depth for test SkolemOccursLoop to 10, for now.

comment:6 Changed 6 years ago by daniel.is.fischer

It's the second part in SkolemOccursLoop, which is the problem.

Judging from the output for small context stacks, what happens is:

We have

type instance G (S x, y) = S (G (x,y))

and the context

(G (S a,a) ~ a)

Generally, a context of the form

G (S a_n, S^n a_n) ~ a_n

By the type instance, that becomes

S (G (a_n, S^n a_n)) ~ a_n

Now, let a_(n+1) = G (a_n, S^n a_n) and replace a_n by (S a_(n+1)) in this:

S (G (S a_(n+1), S^n (S a_(n+1)))) ~ S a_(n+1)

The outermost type constructor S can be removed and we can associate:

G (S a_(n+1), S^(n+1) a_(n+1)) ~ a_(n+1)

The type expression a_n contains 2^n occurrences of a = a_0, hence the size
of the context grows exponentially.
The above takes two stack slots, so size is ~ 2^(stack_depth/2).

That alone would fail hard with a large enough context stack.

What makes it fail sooner, however, is the pretty-printing. According to a couple of +RTS -hT profiles, Pretty.TextBeside takes about 90% of the heap at its peak.

comment:7 Changed 6 years ago by simonpj

Cc: dimitris@… added

comment:8 Changed 6 years ago by igloo

Milestone: 7.4.17.6.1
Priority: normallow

comment:9 Changed 5 years ago by igloo

Milestone: 7.6.17.6.2

comment:10 Changed 3 years ago by thoughtpolice

Milestone: 7.6.27.10.1

Moving to 7.10.1.

comment:11 Changed 3 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:12 Changed 2 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:13 Changed 23 months ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.