Opened 4 years ago

Closed 4 years ago

#8162 closed bug (fixed)

Type unsoundness with type families and UndecidableInstances

Reported by: akio Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.6.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This problem has already been fixed but I'm creating a ticket here to attach an example that demonstrates the problem, following a suggestion here: http://www.haskell.org/pipermail/glasgow-haskell-users/2013-August/022716.html

The following is accepted by GHC 7.6.

type family F a
type instance F (a -> a) = Int
type instance F (a -> a -> a) = IO String

However these definitions allows an Int to be coerced to IO String under UndecidableInstances, breaking type safety. The problem is that you can define an infinite type LA = LA -> LA using type families, then F LA can be reduced to both Int and to IO String.

I'll attach a program that demonstrates how this problem can cause a segfault.

Attachments (4)

Base.hs (825 bytes) - added by akio 4 years ago.
Int_T.hs (144 bytes) - added by akio 4 years ago.
T_IOString.hs (163 bytes) - added by akio 4 years ago.
main.hs (87 bytes) - added by akio 4 years ago.

Download all attachments as: .zip

Change History (5)

Changed 4 years ago by akio

Attachment: Base.hs added

Changed 4 years ago by akio

Attachment: Int_T.hs added

Changed 4 years ago by akio

Attachment: T_IOString.hs added

Changed 4 years ago by akio

Attachment: main.hs added

comment:1 Changed 4 years ago by akio

Resolution: fixed
Status: newclosed
Note: See TracTickets for help on using tickets.