#8162: Type unsoundness with type families and UndecidableInstances -------------------------------------+------------------------------------- Reporter: akio | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.6.3 checker) | Operating System: Unknown/Multiple Keywords: | Type of failure: GHC accepts Architecture: Unknown/Multiple | invalid program Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- ''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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8162 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler