Type family producing infinite type accepted as injective

A question came up during discussion at University of Wrocław:

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.

Trac metadata

Trac field	Value
Version	8.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	goldfire, simonpj
Operating system
Architecture