From 57277662989b97dbf5ddc034d6c41ce39ab674ab Mon Sep 17 00:00:00 2001 From: sheaf Date: Sat, 29 Apr 2023 18:59:10 +0200 Subject: 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 --- libraries/base/GHC/TypeError.hs | 75 +++++++++++++++++++++++++++++++++++------ libraries/base/changelog.md | 4 +++ 2 files changed, 69 insertions(+), 10 deletions(-) (limited to 'libraries') 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 -- cgit v1.2.1