Opened 3 years ago

Closed 2 years ago

Last modified 20 months ago

#9637 closed feature request (fixed)

Type level programming needs an error function

Reported by: augustss Owned by:
Priority: normal Milestone: 8.0.1
Component: Compiler Version: 7.8.3
Keywords: Cc: adamgundry
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #9180, #9636 Differential Rev(s): Phab:D1236
Wiki Page:

Description (last modified by bgamari)

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

Change History (14)

comment:1 Changed 3 years ago by simonpj

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

Simon

comment:2 Changed 3 years ago by augustss

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

comment:3 Changed 3 years ago by 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.

comment:4 Changed 3 years ago by simonpj

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

comment:5 Changed 3 years ago by 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)

comment:6 Changed 3 years ago by adamgundry

Cc: adamgundry added

comment:7 Changed 3 years ago by goldfire

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

comment:8 Changed 2 years ago by simonpj

Description: modified (diff)
Differential Rev(s): Phab:D1236

comment:9 Changed 2 years ago by 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?)

comment:10 Changed 2 years ago by bgamari

Description: modified (diff)
Milestone: 8.0.1

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

comment:11 Changed 2 years ago by 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

comment:12 Changed 2 years ago by bgamari

Resolution: fixed
Status: newclosed

comment:13 Changed 22 months ago by bgamari

I embellished the documentation a bit in 568736d757d3e0883b0250e0b948aeed646c20b5.

comment:14 Changed 20 months ago by 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.

Note: See TracTickets for help on using tickets.