Opened 10 years ago
Closed 8 years ago
#3297 closed bug (fixed)
Compiler panic on incorrect code (TcTyFuns.flattenType: synonym family in a rank-n type)
Reported by: | hesselink | Owned by: | chak |
---|---|---|---|
Priority: | low | Milestone: | 7.2.1 |
Component: | Compiler (Type checker) | Version: | 6.11 |
Keywords: | Cc: | ||
Operating System: | Linux | Architecture: | x86 |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
On the following code sample the compiler panics with:
ghc: panic! (the 'impossible' happened) (GHC version 6.11.20090403 for i386-unknown-linux): TcTyFuns.flattenType: synonym family in a rank-n type
I found this when working on some code when I made a mistake; the code should not type check, but should probably not crash the compiler either. I simplified the code to:
{-# LANGUAGE TypeFamilies , KindSignatures , RankNTypes #-} type family PF a :: (* -> *) -> * -> * class Ix a where type Es a :: * -> * from :: a -> PF a (Es a) a crash :: (forall n. Es a n) -> a crash = from
It seems similar to #3101, but that one was about data types. A similar example also seems to be in #1897, but this bug doesn't seem to fit that ticket's description.
Attachments (1)
Change History (11)
Changed 10 years ago by
comment:1 Changed 10 years ago by
Owner: | set to chak |
---|
The use of a synonym family in a rank-n type is something GHC cannot handle currently. In fact, I am not at all sure how the current approach to type checking with synonym families can be generalised to combine with arbitrary rank-n types (i.e., this is a conceptual, not just an implementation problem). The compiler panic indicates that situation; the error message should be more user-friendly, though.
comment:2 Changed 10 years ago by
difficulty: | → Unknown |
---|
Actually I see no reason in principle why this shouldn't work, but clearly we need to think about the details. Meanwhile a better error message would be a good idea; but even after that's done, let's leave the ticket open until we decide what the long-term answer is.
Simon
comment:3 Changed 10 years ago by
Milestone: | → 6.12.1 |
---|
comment:4 Changed 10 years ago by
Milestone: | 6.12.1 → 6.12 branch |
---|---|
Type of failure: | → None/Unknown |
comment:5 Changed 9 years ago by
Milestone: | 6.12 branch → 6.12.3 |
---|
comment:6 Changed 9 years ago by
Milestone: | 6.12.3 → 6.14.1 |
---|---|
Priority: | normal → low |
comment:7 Changed 9 years ago by
Milestone: | 7.0.1 → 7.0.2 |
---|
comment:8 Changed 9 years ago by
Milestone: | 7.0.2 → 7.2.1 |
---|
comment:9 Changed 9 years ago by
I just tested this with GHC 7.0.2, and the compiler panic is gone. I now get two type errors instead, which is much better. The errors are below.
Temp.hs:13:9: Occurs check: cannot construct the infinite type: uf0 = Es (PF (forall n. uf0 n) (Es (forall n. uf0 n)) (forall n. uf0 n)) Expected type: forall n. Es a n Actual type: forall n. uf0 n Expected type: (forall n. Es a n) -> a Actual type: (forall n. uf0 n) -> PF (forall n. uf0 n) (Es (forall n. uf0 n)) (forall n. uf0 n) In the expression: from In an equation for `crash': crash = from Temp.hs:13:9: Couldn't match type `a' with `PF (forall n. uf0 n) (Es (forall n. uf0 n)) (forall n. uf0 n)' `a' is a rigid type variable bound by the type signature for crash :: (forall n. Es a n) -> a at Temp.hs:13:1 Expected type: (forall n. Es a n) -> a Actual type: (forall n. uf0 n) -> PF (forall n. uf0 n) (Es (forall n. uf0 n)) (forall n. uf0 n) In the expression: from In an equation for `crash': crash = from
comment:10 Changed 8 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Fine. I'll just close this ticket then.
Simon
Code that causes compiler panic