Type unsoundness with type families and UndecidableInstances
|Reported by:||akio||Owned by:|
|Component:||Compiler (Type checker)||Version:||7.6.3|
|Type of failure:||GHC accepts invalid program||Test Case:|
|Related Tickets:||Differential Rev(s):|
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
I'll attach a program that demonstrates how this problem can cause a segfault.