id summary reporter owner description type status priority milestone component version resolution keywords cc os architecture failure testcase blockedby blocking related differential wikipage
11511 Type family producing infinite type accepted as injective jstolarek "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." bug new normal Compiler (Type checker) 8.1 TypeFamilies, InjectiveFamilies goldfire simonpj adamgundry Unknown/Multiple Unknown/Multiple None/Unknown