type-errors (empty) → 0.1.0.0

raw patch · 7 files changed

+518/−0 lines, 7 filesdep +basedep +doctestdep +first-class-familiessetup-changed

Dependencies added: base, doctest, first-class-families, type-errors

Files

• ChangeLog.md +3/−0
• LICENSE +30/−0
• README.md +34/−0
• Setup.hs +2/−0
• src/Type/Errors.hs +354/−0
• test/Main.hs +33/−0
• type-errors.cabal +62/−0

@@ -0,0 +1,3 @@+# Changelog for type-errors++## Unreleased changes

@@ -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.

@@ -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.+

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -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 <https://kcsongor.github.io/ kcsongor>'s @Break@+-- machinery described in+-- <https://kcsongor.github.io/report-stuck-families/ detecting the undetectable>.+--+-- @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+

@@ -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

@@ -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 <https://github.com/isovector/type-errors#readme>+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