GitLab

Closed type families seem to expose as-yet-unexploited opportunities for constraint improvement, one of which I ran into today in the wild. Consider the usual definition of Zip over type level lists:

type family Zip as bs = r | r -> as bs where
  Zip '[]       '[]       = '[]
  Zip (a ': as) (b ': bs) = '(a, b) ': Zip as bs

This type family has an interesting symmetry that could, in theory, be exploited for improvement:

• If we have a constraint [W] a ~ Zip b '[], then we can produce the improvement [D] b ~ '[], since the type family cannot possibly reduce otherwise.

• Similarly, if we have a constraint [W] a ~ Zip b (c ': d), we can produce the improvement [D] b ~ (e ': f), for the same reasons.

Sadly, this does not occur in practice. Consider the following self-contained Haskell program:

{-# LANGUAGE AllowAmbiguousTypes, DataKinds, PolyKinds, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeFamilyDependencies, TypeOperators, UndecidableInstances #-}
module M where

type family Zip as bs = r | r -> as bs where
  Zip '[]       '[]       = '[]
  Zip (a ': as) (b ': bs) = '(a, b) ': Zip as bs

class Null (xs :: [()]) where
  nullT :: Bool
instance Null '[] where
  nullT = True
instance Null (x ': xs) where
  nullT = False

foo :: forall a b. (a ~ Zip b '[], Null b) => Bool
foo = nullT @b

bar :: Bool
bar = foo

On GHC 8.10.2, the above program is rejected with an error:

M.hs:19:7: error:
    • Ambiguous type variable ‘b0’ arising from a use of ‘foo’
      prevents the constraint ‘(Null b0)’ from being solved.
      Probable fix: use a type annotation to specify what ‘b0’ should be.
      These potential instances exist:
        instance Null (x : xs) -- Defined at M.hs:12:10
        instance Null '[] -- Defined at M.hs:10:10

This is unfortunate, as there is only one way this program can possibly typecheck, and it involves instantiating b0 to '[].

Proposed change

It would be ideal if GHC could detect these situations and apply the aforementioned improvements automatically, in the same way it already does in other situations. Improvements would be generated while solving equality constraints where enough equations can be guaranteed apart to yield useful refinements.

Note that I am only proposing additional improvement, not any new evidence. That means the following modified definition of foo from above would still be rejected:

foo :: forall a b. a ~ Zip b '[] => Bool
foo = nullT @b

This is because b is a skolem within the body of foo, not a metavariable. Therefore, we are not at liberty to instantiate it to anything without suitable evidence. By restricting this proposal to improvement, I think it’s conservative enough that a full GHC proposal would be silly; this is not adding anything fundamental, just making a few more programs typecheck.

Potential problems

There is a lingering fear in the back of my mind, which is that stuck type families might make the criteria under which this type of improvement is sound more complicated. For example, suppose we have a constraint like [W] a ~ Zip b '[], where both a and b are metavariables. In certain situations, my understanding is that it’s possible for the program to typecheck without reducing Zip b '[] if a is not “forced” by some other part of the typechecking process.

If that’s true, then it’s theoretically possible for “improvement” of this type to turn a well-typed program into an ill-typed one. If, without improvement, unification eventually instantiates b := (c ': d), then Zip (c ': d) '[] is certainly stuck. But if a is never needed, that could be okay. In that scenario, improvement would create a type error where previously there was none.

I don’t understand the semantics of stuck type families well enough to fully grasp the potential pitfalls here. It seems to me that even if the above were true, perhaps it could be avoided by restricting the situations where improvement applies. However, I think I’d need someone else to chime in to confirm whether or not that is true.