diff options
author | sheaf <sam.derbyshire@gmail.com> | 2023-04-29 18:59:10 +0200 |
---|---|---|
committer | sheaf <sam.derbyshire@gmail.com> | 2023-04-29 20:23:06 +0200 |
commit | 57277662989b97dbf5ddc034d6c41ce39ab674ab (patch) | |
tree | 7d9fe1c4cb95a8bcf82490c354b5df0e9ab9037c /libraries | |
parent | 4eaf2c2a7682fa9933261f5eb25da9e2333c9608 (diff) | |
download | haskell-57277662989b97dbf5ddc034d6c41ce39ab674ab.tar.gz |
Add the Unsatisfiable class
This commit implements GHC proposal #433, adding the Unsatisfiable
class to the GHC.TypeError module. This provides an alternative to
TypeError for which error reporting is more predictable: we report it
when we are reporting unsolved Wanted constraints.
Fixes #14983 #16249 #16906 #18310 #20835
Diffstat (limited to 'libraries')
-rw-r--r-- | libraries/base/GHC/TypeError.hs | 75 | ||||
-rw-r--r-- | libraries/base/changelog.md | 4 |
2 files changed, 69 insertions, 10 deletions
diff --git a/libraries/base/GHC/TypeError.hs b/libraries/base/GHC/TypeError.hs index 77df75854b..21f62afad5 100644 --- a/libraries/base/GHC/TypeError.hs +++ b/libraries/base/GHC/TypeError.hs @@ -1,16 +1,25 @@ {-# LANGUAGE Trustworthy #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MagicHash #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UnboxedTuples #-} {-# LANGUAGE NoImplicitPrelude #-} {-# OPTIONS_HADDOCK not-home #-} {-| -This module exports the TypeError family, which is used to provide custom type -errors, and the ErrorMessage kind used to define these custom error messages. -This is a type-level analogue to the term level error function. +This module exports: + + - The 'TypeError' type family, which is used to provide custom type + errors. This is a type-level analogue to the term level error function. + - The 'ErrorMessage' kind, used to define custom error messages. + - The 'Unsatisfiable' constraint, a more principled variant of 'TypeError' + which gives a more predictable way of reporting custom type errors. @since 4.17.0.0 -} @@ -19,15 +28,15 @@ module GHC.TypeError ( ErrorMessage (..) , TypeError , Assert + , Unsatisfiable, unsatisfiable ) where import Data.Bool import GHC.Num.Integer () -- See Note [Depend on GHC.Num.Integer] in GHC.Base -import GHC.Types (Constraint, Symbol) +import GHC.Types (TYPE, Constraint, Symbol) -{- -Note [Custom type errors] -~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Custom type errors] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ TypeError is used to provide custom type errors, similar to the term-level error function. TypeError is somewhat magical: when the constraint solver encounters a constraint where the RHS is TypeError, it reports the error to @@ -85,9 +94,8 @@ infixl 6 :<>: -- @since 4.9.0.0 type family TypeError (a :: ErrorMessage) :: b where -{- -Note [Getting good error messages from boolean comparisons] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Getting good error messages from boolean comparisons] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We want to write types like f :: forall (x :: Int) (y :: Int). (x <= y) => T x -> T y @@ -139,3 +147,50 @@ type family Assert check errMsg where Assert 'True _ = () Assert _ errMsg = errMsg -- See Note [Getting good error messages from boolean comparisons] + +{- Note [The Unsatisfiable constraint] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The class `Unsatisfiable :: ErrorMessage -> Constraint` provides a mechanism +for custom type errors that reports the errors in a more predictable behaviour +than `TypeError`, as these constraints are handled purely during constraint solving. + +The details are laid out in GHC Proposal #433 (https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst). + +See Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors for +details of the implementation in GHC. + +Note [The Unsatisfiable representation-polymorphism trick] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The class method `unsatisfiableLifted :: forall (a::Type). Unsatisfiable msg => a` +works only for lifted types `a`. What if we want an unsatisfiable value of type +`Int#`, say? The function `unsatisfiable` has a representation-polymoprhic type + unsatisfiable :: forall {rep} (msg :: ErrorMessage) (b :: TYPE rep). + Unsatisfiable msg => b +and yet is defined in terms of `unsatisfiableLifted`. How? By instantiating +`unsatisfiableLifted` at type `(##) -> b`, and applying the result to `(##)`. +Very cunning! +-} + +-- | An unsatisfiable constraint. Similar to 'TypeError' when used at the +-- 'Constraint' kind, but reports errors in a more predictable manner. +-- +-- See also the 'unsatisfiable' function. +-- +-- @since 4.19.0.0@. +type Unsatisfiable :: ErrorMessage -> Constraint +class Unsatisfiable msg where + unsatisfiableLifted :: a + +-- | Prove anything within a context with an 'Unsatisfiable' constraint. +-- +-- This is useful for filling in instance methods when there is an 'Unsatisfiable' +-- constraint in the instance head, e.g.: +-- +-- > instance Unsatisfiable (Text "No Eq instance for functions") => Eq (a -> b) where +-- (==) = unsatisfiable +-- +-- @since 4.19.0.0@. +unsatisfiable :: forall {rep} (msg :: ErrorMessage) (a :: TYPE rep). Unsatisfiable msg => a +unsatisfiable = unsatisfiableLifted @msg @((##) -> a) (##) + -- See Note [The Unsatisfiable representation-polymorphism trick] + diff --git a/libraries/base/changelog.md b/libraries/base/changelog.md index d25888e7fb..bc55cc4977 100644 --- a/libraries/base/changelog.md +++ b/libraries/base/changelog.md @@ -20,6 +20,10 @@ * Add `COMPLETE` pragmas to the `TypeRep`, `SSymbol`, `SChar`, and `SNat` pattern synonyms. ([CLC proposal #149](https://github.com/haskell/core-libraries-committee/issues/149)) * Make `($)` representation polymorphic ([CLC proposal #132](https://github.com/haskell/core-libraries-committee/issues/132)) + * Implemented [GHC Proposal #433](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst), + adding the class `Unsatisfiable :: ErrorMessage -> TypeError`` to `GHC.TypeError`, + which provides a mechanism for custom type errors that reports the errors in + a more predictable behaviour than ``TypeError``. ## 4.18.0.0 *March 2023* * Shipped with GHC 9.6.1 |