diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,3 @@ +# Changelog for type-errors + +## Unreleased changes diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright Author name here (c) 2019 + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Author name here nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,34 @@ +# type-errors + +[![Build Status](https://api.travis-ci.org/isovector/type-errors.svg?branch=master)](https://travis-ci.org/isovector/type-errors) +[![Hackage](https://img.shields.io/hackage/v/type-errors.svg?logo=haskell&label=type-errors)](https://hackage.haskell.org/package/type-errors) + +## Dedication + +> View the gradients of adversity as the colors that paint your story, and the +> power of experience as what makes you a great teacher, creator, philosopher, +> entrepreneur, artist, and human. Everything works out eventually. +> +> Jennifer Sodini + + +## Overview + +`type-errors` is a collection of tools for writing better, more ergonomic, type +errors. Some of the more interesting features are the ability to observe +stuckedness and phantomness, as well as perform substitutions over types. + +For more information, check out the [haddock +documentation](https://hackage.haskell.org/package/type-errors/docs/Type-Errors.html). + + +## Acknowledgments + +This project wouldn't be possible without the help of two amazing people: + +* [ksongor](https://kcsongor.github.io/) who came up with the original + technology behind this library. +* [Lysxia](https://blog.poisson.chat/) for articulating the approach to making + `IfStuck` work for things of all kinds, and for helping me with the + substitution machinery. + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/src/Type/Errors.hs b/src/Type/Errors.hs new file mode 100644 --- /dev/null +++ b/src/Type/Errors.hs @@ -0,0 +1,354 @@ +module Type.Errors + ( -- * Generating Error Messages + ErrorMessage (..) + , PrettyPrintList + , ShowTypeQuoted + + -- * Emitting Error Messages + , TypeError + , DelayError + , DelayErrorFcf + , NoError + , NoErrorFcf + + -- * Observing Stuckness + , IfStuck + , WhenStuck + , UnlessStuck + + -- * Observing Phantomness + , PHANTOM + , UnlessPhantom + , UnlessPhantomFcf + + -- * Performing Type Substitutions + , Subst + , VAR + , SubstVar + + -- * Working With Fcfs + , Exp + , Eval + , Pure + ) where + +import Data.Coerce +import Data.Kind +import Fcf +import GHC.TypeLits + + + +-- $setup +-- >>> :m +Data.Kind +-- >>> :m +Data.Proxy +-- >>> import GHC.Generics (Generic (..)) +-- >>> :def! show_error (\msg -> pure $ "let foo :: DelayError (" ++ msg ++ ") => (); foo = (); in foo") +-- >>> :def! eval_error (\msg -> pure $ "let foo :: (" ++ msg ++ ") => (); foo = (); in foo") +-- >>> :{ +-- data HasNoRep = HasNoRep +-- :} + + +------------------------------------------------------------------------------ +-- | Pretty print a list. +-- +-- >>> :show_error PrettyPrintList '[Bool] +-- ... +-- ... 'Bool' +-- ... +-- +-- >>> :show_error PrettyPrintList '[1, 2] +-- ... +-- ... '1', and '2' +-- ... +-- +-- >>> :show_error PrettyPrintList '["hello", "world", "cool"] +-- ... +-- ... "hello", "world", and "cool" +-- ... +-- +-- @since 0.1.0.0 +type family PrettyPrintList (vs :: [k]) :: ErrorMessage where + PrettyPrintList '[] = 'Text "" + PrettyPrintList '[a] = ShowTypeQuoted a + PrettyPrintList '[a, b] = ShowTypeQuoted a ':<>: 'Text ", and " ':<>: ShowTypeQuoted b + PrettyPrintList (a ': vs) = ShowTypeQuoted a ':<>: 'Text ", " ':<>: PrettyPrintList vs + + +------------------------------------------------------------------------------ +-- | Like 'ShowType', but quotes the type if necessary. +-- +-- >>> :show_error ShowTypeQuoted Int +-- ... +-- ... 'Int' +-- ... +-- +-- >>> :show_error ShowTypeQuoted "symbols aren't quoted" +-- ... +-- ... "symbols aren't quoted" +-- ... +-- +-- @since 0.1.0.0 +type family ShowTypeQuoted (t :: k) :: ErrorMessage where + ShowTypeQuoted (t :: Symbol) = 'ShowType t + ShowTypeQuoted t = 'Text "'" ':<>: 'ShowType t ':<>: 'Text "'" + + +------------------------------------------------------------------------------ +-- | Error messages produced via 'TypeError' are often /too strict/, and will +-- be emitted sooner than you'd like. The solution is to use 'DelayError', +-- which will switch the error messages to being consumed lazily. +-- +-- >>> :{ +-- foo :: TypeError ('Text "Too eager; prevents compilation") => () +-- foo = () +-- :} +-- ... +-- ... Too eager; prevents compilation +-- ... +-- +-- >>> :{ +-- foo :: DelayError ('Text "Lazy; emitted on use") => () +-- foo = () +-- :} +-- +-- >>> foo +-- ... +-- ... Lazy; emitted on use +-- ... +-- +-- @since 0.1.0.0 +type DelayError err = Eval (DelayErrorFcf err) + + +------------------------------------------------------------------------------ +-- | Like 'DelayError', but implemented as a first-class family. +-- 'DelayErrorFcf' is useful when used as the last argument to 'IfStuck' and +-- 'UnlessStuck'. +-- +-- @since 0.1.0.0 +data DelayErrorFcf :: ErrorMessage -> Exp k +type instance Eval (DelayErrorFcf a) = TypeError a + + +------------------------------------------------------------------------------ +-- | A helper definition that /doesn't/ emit a type error. This is +-- occassionally useful to leave as the residual constraint in 'IfStuck' when +-- you only want to observe if an expression /isn't/ stuck. +-- +-- @since 0.1.0.0 +type NoError = (() :: Constraint) + + +------------------------------------------------------------------------------ +-- | Like 'NoError', but implemented as a first-class family. 'NoErrorFcf' is +-- useful when used as the last argument to 'IfStuck' and 'UnlessStuck'. +-- +-- @since 0.1.0.0 +type NoErrorFcf = Pure NoError + + +------------------------------------------------------------------------------ +-- | @'IfStuck' expr b c@ leaves @b@ in the residual constraints whenever +-- @expr@ is stuck, otherwise it 'Eval'uates @c@. +-- +-- Often you want to leave a 'DelayError' in @b@ in order to report an error +-- when @expr@ is stuck. +-- +-- The @c@ parameter is a first-class family, which allows you to perform +-- arbitrarily-complicated type-level computations whenever @expr@ isn't stuck. +-- For example, you might want to produce a typeclass 'Constraint' here. +-- Alternatively, you can nest calls to 'IfStuck' in order to do subsequent +-- processing. +-- +-- This is a generalization of 's @Break@ +-- machinery described in +-- . +-- +-- @since 0.1.0.0 +type family IfStuck (expr :: k) (b :: k1) (c :: Exp k1) :: k1 where + IfStuck (_ AnythingOfAnyKind) b c = b + IfStuck a b c = Eval c + +data AnythingOfAnyKind + + +------------------------------------------------------------------------------ +-- | Like 'IfStuck', but specialized to the case when you don't want to do +-- anything if @expr@ isn't stuck. +-- +-- >>> :{ +-- observe_no_rep +-- :: WhenStuck +-- (Rep t) +-- (DelayError ('Text "No Rep instance for " ':<>: ShowTypeQuoted t)) +-- => t +-- -> () +-- observe_no_rep _ = () +-- :} +-- +-- >>> observe_no_rep HasNoRep +-- ... +-- ... No Rep instance for 'HasNoRep' +-- ... +-- +-- >>> observe_no_rep True +-- () +-- +-- @since 0.1.0.0 +type WhenStuck expr b = IfStuck expr b NoErrorFcf + + +------------------------------------------------------------------------------ +-- | Like 'IfStuck', but leaves no residual constraint when @expr@ is stuck. +-- This can be used to ensure an expression /isn't/ stuck before analyzing it +-- further. +-- +-- See the example under 'UnlessPhantomFcf' for an example of this use-case. +-- +-- @since 0.1.0.0 +type UnlessStuck expr c = IfStuck expr NoError c + + +------------------------------------------------------------------------------ +-- | A meta-variable for marking which argument should be a phantom when +-- working with 'UnlessPhantom' and 'UnlessPhantomFcf'. +-- +-- 'PHANTOM' is polykinded and can be used in several settings. +-- +-- See 'UnlessPhantom' for examples. +-- +-- @since 0.1.0.0 +type PHANTOM = VAR + + +------------------------------------------------------------------------------ +-- | @'UnlessPhantom' expr err@ determines if the type described by @expr@ +-- is phantom in the variables marked via 'PHANTOM'. If it's not, it produces +-- the error message @err@. +-- +-- For example, consider the definition: +-- +-- >>> :{ +-- data Qux a b = Qux b +-- :} +-- +-- which is phantom in @a@: +-- +-- >>> :eval_error UnlessPhantom (Qux PHANTOM Int) ('Text "Ok") +-- () +-- +-- but not in @b@: +-- +-- >>> :eval_error UnlessPhantom (Qux Int PHANTOM) ('Text "Bad!") +-- ... +-- ... Bad! +-- ... +-- +-- Unfortunately there is no known way to emit an error message if the variable +-- /is/ a phantom. +-- +-- @since 0.1.0.0 +type UnlessPhantom exp err = Eval (UnlessPhantomFcf exp err) + + +------------------------------------------------------------------------------ +-- | Like 'UnlessPhantom', but implemented as a first-class family. As such, +-- this allows 'UnlessPhantomFcf' to be chained after 'IfStuck' to only be run +-- if an expression isn't stuck. +-- +-- This can be used to avoid emitting false error messages when a type variable +-- isn't phantom, just ambiguous. +-- +-- >>> :{ +-- observe_phantom +-- :: UnlessStuck +-- f +-- (UnlessPhantomFcf +-- (f PHANTOM) +-- ('Text "It's not phantom!")) +-- => f p +-- -> () +-- observe_phantom _ = () +-- :} +-- +-- >>> observe_phantom Proxy +-- () +-- +-- >>> observe_phantom (Just 5) +-- ... +-- ... It's not phantom! +-- ... +-- +-- In the next example, we leave @observe_phantom@ unsaturated, and therefore +-- @f@ isn't yet known. Without guarding the 'UnlessPhantomFcf' behind +-- 'UnlessStuck', this would incorrectly produce the message "It's not +-- phantom!" +-- +-- >>> observe_phantom +-- ... +-- ... No instance for (Show ... +-- ... +-- +-- @since 0.1.0.0 +data UnlessPhantomFcf :: k -> ErrorMessage -> Exp Constraint +type instance Eval (UnlessPhantomFcf exp err) = + Coercible (SubstVar exp Stuck) + (SubstVar exp (DelayError err)) + + +------------------------------------------------------------------------------ +-- | @'Subst' expr a b@ substitutes all instances of @a@ for @b@ in @expr@. +-- +-- >>> :kind! Subst (Either Int Int) Int Bool +-- ... +-- = Either Bool Bool +-- +-- >>> :kind! Subst (Either Int Bool) Int [Char] +-- ... +-- = Either [Char] Bool +-- +-- >>> :kind! Subst (Either Int Bool) Either (->) +-- ... +-- = Int -> Bool +-- +-- @since 0.1.0.0 +type family Subst (e :: k1) (var :: k2) (sub :: k2) :: k1 where + Subst var var sub = sub + Subst (a b) var sub = Subst a var sub (Subst b var sub) + Subst a var sub = a + +data Var +type family SubMe :: Type -> k + +------------------------------------------------------------------------------ +-- | 'VAR' is a meta-varaible which marks a substitution in 'SubstVar'. The +-- result of @'SubstVar' expr val@ is @expr[val/'VAR']@. +-- +-- 'VAR' is polykinded and can be used in several settings. +-- +-- See 'SubstVar' for examples. +-- +-- @since 0.1.0.0 +type VAR = SubMe Var + + +------------------------------------------------------------------------------ +-- | Like 'Subst', but uses the explicit meta-variable 'VAR' to mark +-- substitution points. +-- +-- >>> :kind! SubstVar (Either VAR Bool) [Char] +-- ... +-- = Either [Char] Bool +-- +-- >>> :kind! SubstVar (VAR Int Bool :: Type) (->) +-- ... +-- = Int -> Bool +-- +-- @since 0.1.0.0 +type family SubstVar (e :: k1) (r :: k2) :: k1 where + SubstVar (_ Var) r = r + SubstVar (a b) r = SubstVar a r (SubstVar b r) + SubstVar a r = a + diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE CPP #-} + +module Main where + +import Test.DocTest + + +main :: IO () +#if __GLASGOW_HASKELL__ < 804 +main = pure () +#else +main = doctest + [ "-isrc/" + , "--fast" + , "-package first-class-families" + , "-XConstraintKinds" + , "-XDataKinds" + , "-XKindSignatures" + , "-XPolyKinds" + , "-XScopedTypeVariables" + , "-XTypeFamilies" + , "-XTypeOperators" + , "-XUndecidableInstances" + , "-XTypeApplications" + , "-XFlexibleContexts" + +#if __GLASGOW_HASKELL__ < 806 + , "-XTypeInType" +#endif + + , "src/Type/Errors.hs" + ] +#endif diff --git a/type-errors.cabal b/type-errors.cabal new file mode 100644 --- /dev/null +++ b/type-errors.cabal @@ -0,0 +1,62 @@ +cabal-version: 1.12 + +-- This file has been generated from package.yaml by hpack version 0.31.2. +-- +-- see: https://github.com/sol/hpack +-- +-- hash: c34b99cb7785b40b9930c5de60ab842dfd436ec4458a51b595b426da5fcd4a3f + +name: type-errors +version: 0.1.0.0 +synopsis: Tools for writing better type errors +description: Please see the README on GitHub at +category: Type +homepage: https://github.com/isovector/type-errors#readme +bug-reports: https://github.com/isovector/type-errors/issues +author: Sandy Maguire +maintainer: sandy@sandymaguire.me +copyright: 2019 Sandy Maguire +license: BSD3 +license-file: LICENSE +build-type: Simple +extra-source-files: + README.md + ChangeLog.md + +source-repository head + type: git + location: https://github.com/isovector/type-errors + +library + exposed-modules: + Type.Errors + other-modules: + Paths_type_errors + hs-source-dirs: + src + default-extensions: ConstraintKinds DataKinds PolyKinds ScopedTypeVariables TypeFamilies TypeOperators UndecidableInstances TypeApplications FlexibleContexts + ghc-options: -Wall + build-depends: + base >=4.7 && <5 + , first-class-families >=0.5.0.0 + if impl(ghc < 8.6) + default-extensions: TypeInType + default-language: Haskell2010 + +test-suite test + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: + Paths_type_errors + hs-source-dirs: + test + default-extensions: ConstraintKinds DataKinds PolyKinds ScopedTypeVariables TypeFamilies TypeOperators UndecidableInstances TypeApplications FlexibleContexts + ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N + build-depends: + base >=4.7 && <5 + , doctest >=0.16.0.1 && <0.17 + , first-class-families >=0.5.0.0 + , type-errors + if impl(ghc < 8.6) + default-extensions: TypeInType + default-language: Haskell2010