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)

crash.hs (263 bytes) - added by hesselink 10 years ago.
Code that causes compiler panic

Download all attachments as: .zip

Change History (11)

Changed 10 years ago by hesselink

Attachment: crash.hs added

Code that causes compiler panic

comment:1 Changed 10 years ago by chak

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 simonpj

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 igloo

Milestone: 6.12.1

comment:4 Changed 10 years ago by igloo

Milestone: 6.12.16.12 branch
Type of failure: None/Unknown

comment:5 Changed 9 years ago by igloo

Milestone: 6.12 branch6.12.3

comment:6 Changed 9 years ago by igloo

Milestone: 6.12.36.14.1
Priority: normallow

comment:7 Changed 9 years ago by igloo

Milestone: 7.0.17.0.2

comment:8 Changed 9 years ago by igloo

Milestone: 7.0.27.2.1

comment:9 Changed 9 years ago by hesselink

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 simonpj

Resolution: fixed
Status: newclosed

Fine. I'll just close this ticket then.

Simon

Note: See TracTickets for help on using tickets.