Undecidable instances slip through
Consider
{-# LANGUAGE FlexibleInstances, TypeFamilies, ConstraintKinds #-}
type family F a :: Constraint
class C a where
instance (F a) => C [[a]] where
This should be rejected because the F a
constraint could expand to be arbitrarily large, depending on F
.
But it's accepted by HEAD. There's simply a missing check in checkInstTermination
.