[GHC] #11511: Type family producing infinite type accepted as injective

[GHC]

#11511: Type family producing infinite type accepted as injective
-------------------------------------+-------------------------------------
           Reporter:  jstolarek      |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           Keywords:  TypeFamilies,  |  Operating System:  Unknown/Multiple
  Injective                          |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 A question came up during discussion at University of Wrocław:


 {{{#!hs
 type family F a = r | r -> a where
     F a = [F a]
 }}}

 Should this pass the injectivity check? Currently it does but I don't
 think this is correct. After all `F Bool` and `F Char` both reduce to the
 same infinite type `[[[...]]]`, which by definition of injectivity gives
 us `Char ~ Bool`. Is this dangerous in practice? It can cause reduction
 stack overflow (or an infinite loop if you disable that check) but I don't
 think this can be used to construct unsafe coerce. We'd have to unify two
 infinite types, which does not seem possible.

 This is not an implementation problem - this stays faithful to theory
 developed in injective type families paper. If others agree that this is
 indeed incorrect then I think the right solution here would be to drop
 equation (7) from our algorithm in the paper. For generalized injectivity
 we planned drop that equation anyway. Here's another reason for doing
 this.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11511>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler