GitLab

There's a subtle issue going on with injective type families. Simply reordering the arguments can cause an otherwise legal program to hang on compile. Calling f_bad instead of f_good will cause the compiler to hang, looping forever in the typechecker, but the only difference between TF_Good and TF_Bad is that the argument order is swapped.

{-# LANGUAGE TypeFamilyDependencies #-}

main = return $ f_good (Just 'c')
--main = return $ f_bad (Just 'c')

type family TF x y = t | t -> x y
type instance TF Int Float = Char

type family TF_Good x y = t | t -> x y
type instance TF_Good a (Maybe x) = Maybe (TF a x)

f_good :: TF_Good a x -> ()
f_good _ = ()

type family TF_Bad x y = t | t -> x y
type instance TF_Bad (Maybe x) a = Maybe (TF a x)

f_bad :: TF_Bad x a -> ()
f_bad _ = ()