[GHC] #8162: Type unsoundness with type families and UndecidableInstances

[GHC]

#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