Type level programming needs an error function

[augustss]

When doing type level programming you often need a way to report errors. I suggest a closed type family called Error with special semantics. It is kinded like this Error :: Symbol -> k1 -> k2

If this function has to be reduced during constraint solving it will simply generate a type error with the given string and printing the type as extra information (this kind can be generalized a lot if we want to).

I've found that having this function gives more accurate and earlier error messages.

Wiki design page: Proposal/CustomTypeErrors

[simonpj]

I'm all for it! Can you write a more precise specification?

Simon

[augustss]

I'll experiment and see what seems to work well in the Mu compiler.

[augustss]

Here's what I'm using now, and it works nicely. But better names would be nice.

type family Error (a :: k1) :: k2 where { }
data ErrorAnd (a :: k1) (b :: k2)

When the type checker encounters the Error function it generates the error message according to the following pseudo code:

flatten (Symbol s) = s
flatten (ErrorAnd t1 t2) = flatten t1 ++ flatten t2
flatten t = prettyPrint t

So for instance Error "Oh noes!" will generate the error message "Oh noes!". And Error ("Mismatch between " `ErrorAnd` t1 `ErrorAnd` " and " `ErrorAnd` t2) will generate "Mismatch between ... and ...", where ... are the pretty printing of the types t1 and t2 respectively.

[simonpj]

Can you give some examples of its use in a program? I still don't get it.

[augustss]

Here's a real example:

type F_NoDups (t :: FieldSet) :: FieldSet =
    Assert "Type has duplicate labels:\n  " (Not (F_HasDups t)) t

type family Assert (msg :: Symbol) (a :: Bool) (b :: k) :: k where
     Assert msg True  x = x
     Assert msg False x = Error (msg `ErrorAnd` x)

And here's a sample error message:

RunMu.exe: Cortex: Cortex.Stem.Relation.Test.Typed:21:1: Type error:
Type has duplicate labels:
  Cortex.Stem.Relation.Types.FS
    ("A" ::: String : "B" ::: Bool : "B" ::: Bool : "C" ::: () : Data.TypeLevel.Nil)

[goldfire]

#9180 proposes a similar mechanism at the term level. #9636 is a nice application of the feature proposed in this ticket.

[simonpj]

On the implementation front, I have some suggestions, which I've added under SLPJ alternative design on the wiki page CustomTypeErros

(The title of the wiki page is mis-spelled. Rename?)

[bgamari]

It sounds like this will make it in for 8.0.1 with an implementation by Iavor Diatchki. Thanks Iavor!

[Ben Gamari <ben@…>]

In 2d1a563/ghc:

Implement support for user-defined type errors.

Implements Lennart's idea from the Haskell Symposium.
Users may use the special type function `TypeError`, which is
similar to `error` at the value level.

See Trac ticket https://ghc.haskell.org/trac/ghc/ticket/9637, and wiki
page https://ghc.haskell.org/trac/ghc/wiki/CustomTypeErros

Test Plan: Included testcases

Reviewers: simonpj, austin, hvr, goldfire, bgamari

Reviewed By: goldfire, bgamari

Subscribers: adamgundry, thomie

Differential Revision: https://phabricator.haskell.org/D1236

GHC Trac Issues: #9637

[bgamari]

I embellished the documentation a bit in 568736d757d3e0883b0250e0b948aeed646c20b5.

[Lemming]

I just want to add: The Helium people also thought about customizing error messages: See Heeren, Hage, Swierstra on ​Scripting the Type Inference Process.