Opened 10 years ago

Closed 9 years ago

#3484 closed bug (fixed)

GHC diverges when proving nonequality of types

Reported by: ryani Owned by:
Priority: low Milestone: 7.0.1
Component: Compiler Version: 6.10.4
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/indexed-types/T3484
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Conor posted an interesting suggestion for proving type non-equality here:

http://www.nabble.com/Re%3A-Is-it-possible-to-prove-type-*non*-equality-in-Haskell--p25153135.html

I implemented it on my Nat framework and got GHC to diverge:

C:\haskell>ghc -c Absurd.hs
stack overflow: use +RTS -K<size> to increase it

I've attempted to shrink the code as much as possible and still reproduce the error; attached is the result.

Attachments (1)

absurd.hs (1.4 KB) - added by ryani 10 years ago.

Download all attachments as: .zip

Change History (7)

Changed 10 years ago by ryani

Attachment: absurd.hs added

comment:1 Changed 10 years ago by chak

We should probably document this somewhere: we know nothing about the properties of programs combining type families and rank-n types. It wouldn't surprise me if some of these programs lead to the type checker diverging. In other words, solving this problem likely requires some serious research into type systems combining type families and rank-n types.

comment:2 Changed 10 years ago by simonpj

difficulty: Unknown

It's true that we have not explicitly thought about higher rank, but I'm still surprised at divergence. Let's leave this open and on the type-families list, so that we remember to get back to it.

Simon

comment:3 Changed 10 years ago by igloo

Milestone: 6.12 branch

comment:4 Changed 9 years ago by igloo

Milestone: 6.12 branch6.12.3

comment:5 Changed 9 years ago by igloo

Milestone: 6.12.36.14.1
Priority: normallow

comment:6 Changed 9 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: typecheck/indexed-types/T3484
Type of failure: None/Unknown

Happily this now works fine in the HEAD. I've added a regression test.

Note: See TracTickets for help on using tickets.