One classic appeal of Haskell is that its type system allows experts to define very precise constraints within the program’s problem domain. In my working experience, such powerful constraints are a double-edged sword for projects with long lifespans. These sophisticated types do, as promised, statically prevent many kinds of costly mistakes and are indeed expressed via definitions that resemble the particular problem domain better than many other general purpose languages would allow. On the other hand, the requisite definitions tend to be dense and leak noisy details of how exactly the domain-specific constraints were encoded in the GHC Haskell type system. This is sadly often apparent in the poor quality of error messages that arise when these type-level programs catch a user’s mistake. So while use of these precise problem-specific types provides very desirable static checks, they also often frustrate or intimidate less expert contributors — including the original authors when they return to the project after a few months!

In this post, I present a technique that can help mitigate that downside. I call the technique Ill-Formedness Indicators. For a broad class of domain-specific constraints/languages, this is the first technique I’ve learned of that enables custom compile-time error messages in the particularly insidious scenario where the user’s mistake incurs polymorphism that the library author did not intend. I’ll explain with a small and concrete example and then list some generalizations that would also benefit from Ill-Formedness Indicators in the exact same way.

The mechanism underlying Ill-Formedness Indicators is introduced by Csongor Kiss’s blog post Detecting the undetectable: custom type errors for stuck type families. My contribution is to emphasize that it applies to type classes in addition to type families, and to spell out how and when it can be applied.

The complete and self-contained code for this blog post can be found here.

Motivation

My working example for this technique is the definition of a smart constructor for the conventional heterogeneous vector data type. I include the signature of the vrev function here only for completeness; its definition is uninteresting.

data Vec :: [Type] -> Type where
    VNil  ::                Vec '[]
    VCons :: x -> Vec xs -> Vec (x : xs)

-- | Reverse the vector
vrev :: VRev xs xs' => Vec xs -> Vec xs'

My example smart constructor is named litVec. It’s smart because it can be applied to any number of arguments. In Haskell, such variadic functions can only be defined via type-level programming, which is why litVec is a useful example for this blog post.

Here are some examples of the intended use of litVec and its auxiliary function variadic, which merely delineates the end of the variable-length list of arguments. Unfortunately, neither has a helpful type signature, as you will see in the small definition immediately below.

> :type variadic (litVec 'c' True 3)
variadic (litVec 'c' True 3)
  :: Num t => Vec '[Char, Bool, t]
> variadic (litVec 'c' True 3)
VCons 'c' (VCons True (VCons 3 VNil))
> variadic $ litVec 'c' True
VCons 'c' (VCons True VNil)
> variadic (litVec True)
VCons True VNil
> variadic litVec
VNil

This first definition of litVec does not use an Ill-Formedness Indicator, so that its misbehavior can motivate that enrichment.

{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances,
             MultiParamTypeClasses, TypeFamilies, TypeOperators,
             UndecidableInstances #-}

module LitVec (litVec, variadic) where

import Vec (Vec (VCons, VNil), VRev (vrev))

-- | NOT EXPORTED
class MkLitVec xs a where mkLitVec :: Vec xs -> a

instance MkLitVec (x : xs) a => MkLitVec xs (x -> a) where
    mkLitVec acc = \x -> mkLitVec (VCons x acc)

-- | NOT EXPORTED
newtype Variadic a = MkVariadic { {- | See 'litVec' -} variadic :: a }

instance (VRev xs xs', a ~ Vec xs') => MkLitVec xs (Variadic a) where
    mkLitVec acc = MkVariadic (vrev acc)

-- | A variadic vector constructor
--
-- Use it like this: @'variadic' ('litVec' a b c)@
litVec :: MkLitVec '[] a => a
litVec = mkLitVec VNil

In words: the first instance handles each argument to litVec, and the second instance handles when the user finally applies variadic, which indicates there will be no further arguments. The first instance merely pushes the arguments on to a stack, and the second instance reverses that stack to yield the final vector in the same left-to-right order that the user wrote the arguments in. Only litVec and variadic need be exported; they constitute the entire interface supporting the intended use.

The key mistake the user can make would be to use litVec without the application of variadic. The variadic function is how the user delimits the end of the arguments to litVec. Together that pair of identifiers effectively provides literal syntax for the Vec type, and so is analogous to the pair of [ and ] for lists. (It’s a very small change to instead enable the syntax beginVec x y z endVec, but as far as I know that requires -XIncoherentInstances, which would necessitate a tangential explanation of its own.)

If the user is confused or simply forgets to call variadic, ideally GHC would tell them as much, just as it does when they forget the ] for a list literal. Unfortunately, that is not the case with the above conventional definition of litVec.

> litVec 'c' True 3

<interactive>:23:1: error:
    • Could not deduce (MkLitVec '[t0, Bool, Char] t1)
      from the context: (MkLitVec '[t, Bool, Char] t1, Num t)
        bound by the inferred type for ‘it’:
                   forall t t1. (MkLitVec '[t, Bool, Char] t1, Num t) => t1
        at <interactive>:23:1-16
      The type variable ‘t0’ is ambiguous
    • In the ambiguity check for the inferred type for ‘it’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the inferred type
        it :: forall t1 t2. (MkLitVec '[t1, Bool, Char] t2, Num t1) => t2

Nothing about that error message indicates that the user forgot to apply variadic. Worse still, the message actually recommends the AllowAmbiguousTypes language extension, which is notorious for tricking novice users into deferring the error message to the call-site, much farther away from their actual mistake! An expert would eventually intuit the problem, but, without revisiting the definition of MkLitVec, even they would fail to determine the intended use requires variadic.

Thus this definition of litVec is a disappointment; library users should not have to inspect the implementation details in order to understand the error message induced by a simple and common mistake. This is the problem that Ill-Formedness Indicators let the library author solve. The only other way I know for a library author to address this kind of mistake is to warn about it loudly in the library documentation. In my opinion, that option fails to meet the Haskell community’s general expectations around type safety.

Demonstration

Once I add Ill-Formedness Indicators to the definition of litVec, the user instead sees the following custom compile-time error message, which explains the exact mistake we’re targeting.

> litVecIFI 'c' True 3

<interactive>:25:1: error:
    • Likely accidental use of `litVecIFI' outside of `variadic'!
    • When checking the inferred type
        it :: forall t1 t2.
              (MkLitVecIFI (TypeError ...) '[t1, Bool, Char] t2, Num t1) =>
              t2

Ill-Formedness Indicators can be summarized in a single sentence.

The library author must ensure that any constraint they never want the user to see includes a subexpression that is an application of the special TypeError family introduced in GHC 8.0.2 to the desired error message.

That subexpression is the eponymous indicator. If one is present in a constraint that the typechecker couldn’t simplify where it originally arose, then that TypeError will trigger when GHC is checking the inferred type. This ensures the user sees the bespoke error message instead of the standard Could not deduce error that contains the inscrutable implementation details of the internal constraints, which the library author would rather users never have to consider.

The enriched definition of litVecIFI is very similar to the original litVec definition above: I only need to add a Void parameter to the class, propagate it, and initialized it with a specific TypeError in the signature of litVecIFI. My specific recommendation for Ill-Formedness Indicators is — whenever possible — to add a new parameter of kind Void to the type classes used in internal constraints and confine the indicator TypeError arguments to that new parameter. Even in more sophisticated use cases where some pre-existing parameters might already be able to host the indicators, I favor adding a new argument of kind Void in order to more cleanly separate the encoding noise of the Ill-Formedness Indicators from the classes’ actual logic. The Void kind (ideally) has no “matchable” inhabitants, which ensures it cannot influence instance selection for its class.

-- | NOT EXPORTED
class MkLitVecIFI (ifi :: Data.Void.Void) xs a where
    mkLitVecIFI :: Proxy ifi -> Vec xs -> a

instance MkLitVecIFI ifi (x : xs) a => MkLitVecIFI ifi xs (x -> a) where
    mkLitVecIFI ifi acc = \x -> mkLitVecIFI ifi (VCons x acc)

-- | NOT EXPORTED
newtype Variadic a = MkVariadic { {- | See 'litVecIFI' -} variadic :: a }

instance (a ~ Vec xs', VRev xs xs') => MkLitVecIFI ifi xs (Variadic a) where
    mkLitVecIFI _ifi acc = MkVariadic (vrev acc)

-- | A variadic vector constructor
--
-- Use it like this: @'variadic' ('litVecIFI' a b c)@
litVecIFI :: MkLitVecIFI (DelayTypeError LitVecErrMsg) '[] a => a
litVecIFI = mkLitVecIFI (Proxy :: Proxy (DelayTypeError LitVecErrMsg)) VNil

type LitVecErrMsg =
  GHC.TypeLits.Text
    "Likely accidental use of `litVecIFI' outside of `variadic'!"

-- | If I directly used 'TypeError' above instead of 'DelayTypeError', GHC
-- would raise the error while typechecking the 'litVecIFI' definition. This
-- alias's single layer of indirection is enough to prevent that.
-- <https://gitlab.haskell.org/ghc/ghc/-/issues/20241> should happily supplant
-- this in future GHCs.
--
-- Note: this can be defined elsewhere and reused amongst many uses of
-- Ill-Formedness Indicators.
type family DelayTypeError (err :: ErrorMessage) :: Void where
    DelayTypeError err = GHC.TypeLits.TypeError err

That’s all there is to it, just the extra class parameter and the concrete error messages. The user will now see the clear and helpful error message when they forget to apply variadic, as shown at the top of this section.

Ill-Formedness Indicators do unavoidably add some noise to the definitions, but it is minimal, merely propagating through the Void parameter. Only a new GHC language extension, pragma, or similar could further reduce the boilerplate.

Why It Works

Csongor Kiss’s blog post explains the actual mechanics in detail. If only for the sake of self-containedness, I complement that here by providing a higher-level explanation.

In general, Ill-Formedness Indicators provide a way to opt-out of Haskell’s open-world assumption for some constraints, such as the constraint in the signature of litVecIFI. When type-checking, if a value definition requires some constraints that are not fully solved by whatever instance declarations are already in-scope, GHC infers the definition has type cx => ... where cx is the residual constraints. That inference is justified by the open-world assumption, which acknowledges that a call site might concretize some of the type variables so that those same instances now suffice or it could merely have more instances in-scope. And if the constraint is still stuck at the call site, then the cycle repeats: GHC will also infer a type context for that enclosing definition, which has its own call sites, and so on. This cycle only stops under two circumstances. Either it reaches a point in the program where constrained types are not allowed, such as an executable’s main entrypoint, the Read-Eval-Print-Loop, or a signature written by the user, or else GHC identifies one of the residual constraints as insoluble (e.g., Int ~ Bool). In other words, the cycle stops when (the relevant part of) the world has become closed instead of open.

Indeed, the motivating example from the previous section emitted the Could not deduce error message only because I entered the expression at the REPL prompt. If I instead were to bound that litVec-without-variadic to a definition, then there would be no error at all without Ill-Formedness Indicators.

> let foo z = litVec 'c' True z
> :info foo
foo :: MkLitVec '[t1, Bool, Char] t2 => t1 -> t2

Such inferred types might prove even more confusing than the bad error message! Eventually an error message would arise, but it will not be local to the actual mistake (just like -XAllowAmbiguousTypes above). Or the user might inspect the inferred type and be confused about its meaning — recall that the library author never intended for them to consider it. The inferred context is not that noisy in this small litVec example, but it would quickly become overwhelmingly dense in more real-world applications involving type-level programming.

With Ill-Formedness Indicators the user instead sees the same bespoke error in either example — they see it whenever they fail to apply variadic to the litVec application, full stop. This is the sort of predictable simple behavior that lets a library author guide their users with in-band advice. In particular, the user sees the error despite the fact that a later call site could apply variadic, thereby eliminating the error altogether — i.e., despite GHC’s open-world assumption.

> let foo z = litVecIFI 'c' True z

<interactive>:33:5: error:
    • Likely accidental use of `litVecIFI' outside of `variadic'!
    • When checking the inferred type
        foo :: forall t1 t2.
               MkLitVecIFI (TypeError ...) '[t1, Bool, Char] t2 =>
               t1 -> t2

In this way, an Ill-Formedness Indicator opts-out of GHC’s open-world assumption, but only for the MkLitVec constraint in the declared signature of litVec.

The low-level mechanics depends on GHC’s special treatment of TypeError applications. In particular, TypeError exhibits negation-as-failure semantics, which is a hallmark of the closed-world assumption. Moreover, beyond a merely insoluble constraint, a TypeError application anywhere within a constraint in an inferred context causes GHC to raise the compile-time error. Ill-Formedness Indicators wouldn’t help nearly as much if TypeError had to be at the head of the stuck constraint (which is what I had been incorrectly assuming would be necessary before reading Kiss’s blog post — and is what the proposed Unsatisfiable family will do), since GHC’s open-world assumption makes it difficult to robustly emit a TypeError-headed constraint only when the constraint is stuck.

Alternatives

The only alternative I am aware of relies on overlapping instances. For my original example, this would require merely one additional instance, using the OVERLAPS pragma.

class MkLitVecOI xs a where mkLitVecOI :: Vec xs -> a

instance {-# OVERLAPS #-} MkLitVecOI (x : xs) a => MkLitVecOI xs (x -> a) where ...

instance {-# OVERLAPS #-} (a ~ Vec xs', VRev xs xs') => MkLitVecOI xs (Variadic a) where ...

-- I could have instead used `OVERLAPPABLE` here, but `OVERLAPS` on the other
-- instances better conveys the intention. In cases where the type class is
-- exported, some well-intentioned but confused expert users may interpret an
-- `OVERLAPPABLE` pragma as an invitation to declare their own instances.
instance TypeError LitVecErrMsg => MkLitVecOI xs a where
    mkLitVecOI = error "unreachable code!"

This approach has one advantage over Ill-Formedness Indicators and a few significant disadvantages. The advantage is that it involves much less noise/boilerplate and especially that it does not need to alter the class definition. The disadvantages are as follows:

• Overlapping instances is not a trivial language extension; it introduces its own pitfalls, complexities, etc. Those aren’t apparent in this small MkLitVecOI example, but could be in more sophisticated domain-specific logics.
• The open-world assumption requires that GHC can infer the constraint MkLitVecOI xs a without raising an error, which means this instance-triggered approach could not robustly enforce my simple desideratum of “litVecOI must always occur inside of variadic, full stop”, unless every call site occurred in a definition that has a user-written signature. Such pervasive signatures are often encouraged by standard coding styles, but it’s not guaranteed, and especially not during active development. GHC would most likely eventually raise the error (worst-case: in the library users’ builds), but the greater the number of unascribed definitions between the error message’s location and the mistake, the more confusing the custom error message’s location information would be. And thus I don’t consider that robust.
• Sometimes the domain-specific logic already relies on overlapping instances. It may deserve more thought, but I haven’t already convinced myself that one can always add a set of overlapping instances that perfectly complement some domain-specific logic’s actual instances when some of those already rely on the overlapping instances language extension.

In my opinion, those disadvantages generally outweigh the advantage of less noise. Moreover, in this case, that MkLitVecIFI class is an internal implementation detail, so noise there wouldn’t affect the user, though it could, in general, make it harder for the developer to maintain the library. On the other hand, the addition of the single err type parameter and its propagation does seem mild to me; especially when the domain-specific constraints are already themselves big, which is likely compared to the intentionally small litVec example.

When to Use It

I anticipate Ill-Formedness Indicators are applicable in any type-level programming that shares at least one of the following characteristics of litVec.

• I intend for litVec and variadic to feel like a new syntactic construct. If the user applies my combinators in an ill-formed way, then I don’t want GHC to grant it a value or even a type: I’d rather show a “parse error”.

• I define the combinators’ semantics via a type class, but it is not my intent for the user to ever consider that class: they are not to instantiate it, not to include it in their signatures, etc.

• Instead, any well-formed use of the combinators should only incur internal constraints that the instances in-scope at the call site fully resolve. Note that the internal constraints do not necessarily need to resolve all the way to True but merely down to a set of non-internal constraints, those that are intended for the user to see. In other words, I want GHC to use a very specific closed-world assumption: it should assume that the call site’s in-scope instances include all the instances that could possibly reduce the internal constraints. While my litVec example doesn’t involve the user declaring new such instances, a more sophisticated use case might intentionally allow for (power) users to do so, and such instances should also be considered at call sites. It’s subtle that the set of relevant instances can exhibit both extensibility and a closed-world assumption, but that’s only necessary in advanced usage.

Concretely, my colleagues at Tweag have identified a few use cases in the wild.

• Facundo Domínguez notes that the inline-java package uses the OVERLAPPABLE alternative discussed above for its variadic functions. This is usually sufficient, since standard practice involves writing pervasive top-level signatures. But it does invite the occasional unexpectedly inferred Variadic_ constraint when used at the REPL prompt or in uses relying more heavily on inference. An Ill-Formedness Indicator would work even in those scenarios.

• Alexander Esgen added an Ill-Formedness Indicator in the servant package to improve the user experience when the user tries to use a part of the Servant API for named routes but forgot the required instance of GHC.Generics.Generic.

• One recent idea, with Christian Georgii, leaned heavily on type-level programming to validate that the user indeed declared a bijection between two enumeration data types. Just like MkLitVec et al, the user is never intended to consider the classes and instances encoding the mathematical definition of a bijection, but the classes show up whenever the user makes a typo, forgets to include a matched pair in the specified bijection, accidentally maps two pre-images to the same image, adds a new constructor to one of the corresponding data types, etc. Ill-Formedness Indicators can be mechanically added to improve the error messages to specify exactly why the user’s expression is not actually a bijection as intended.

Conclusion

Ill-Formedness Indicators enable library authors doing type-level programming to improve their users’ experience when the user applies the library’s combinators in a way that involves more polymorphism than the author intended.

Though an Ill-Formedness Indicator is merely a careful use of TypeError, it’s a clever trick that I hadn’t considered before seeing Csongor Kiss’s blog post, despite being aware for many years of both TypeError and the sorts of disappointing user experiences that Ill-Formedness Indicators address.

I can recommend Ill-Formedness Indicators despite their cleverness because the whole point is that they can be used to hide implementation details — aka “too much cleverness” — from the user experience. My only reservation in recommending it is that TypeError itself is perhaps too immature.

• I know no way to predict exactly when TypeError will trigger other than combing through the code of GHC’s typechecker (e.g., this commit). This behavior should instead be more explicitly specified in the user guide. An Ill-Formedness Indicator depends on TypeError triggering under certain circumstances; I think those are fundamental to TypeError’s behavior and so unlikely to change, but I can’t be sure without the missing TypeError specification.

• When GHC detects a TypeError, it suppresses some other flavors of error. In some of my more aggressive experiments with Ill-Formedness Indicators, this has lead to some confusingly opaque custom error messages; because of the Ill-Formedness Indicator’s error message, GHC suppressed the error message that would have helped me identify my actual mistake. My workaround so far has been to remove the DelayTypeError err = TypeError err instance while debugging an Ill-Formedness Indicator message that makes no sense to me. Doing so completely disables the Ill-Formedness Indicators, but it sometimes reveals the other flavors of errors that were being suppressed. This could be more conveniently enabled with a -fdisarm-TypeError flag to GHC, etc. I suppose the tiers of error messages are there for a good reason, but a similar GHC flag, etc. to prevent such error suppression might also help in these cases.

I hope you find Ill-Formedness Indicators useful as you squeeze as much safety and quality of life as possible out of GHC!