{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}

-----------------------------------------------------------------------------

-----------------------------------------------------------------------------

-- |
-- Module      :  Disco.Error
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Type for collecting all potential Disco errors at the top level,
-- and a type for runtime errors.
module Disco.Error (DiscoError (..), EvalError (..), panic, outputDiscoErrors) where

import Prelude hiding ((<>))

import Text.Megaparsec (
  ParseErrorBundle,
  errorBundlePretty,
 )
import Unbound.Generics.LocallyNameless (Name)

import Disco.Effects.LFresh
import Polysemy
import Polysemy.Error
import Polysemy.Output
import Polysemy.Reader

import Disco.Messages
import Disco.Names (ModuleName, QName)
import Disco.Parser (DiscoParseError)
import Disco.Pretty
import Disco.Typecheck.Solve
import Disco.Typecheck.Util (
  LocTCError (..),
  TCError (..),
 )
import Disco.Types
import Disco.Types.Qualifiers

-- | Top-level error type for Disco.
data DiscoError where
  -- | Module not found.
  ModuleNotFound :: String -> DiscoError
  -- | Cyclic import encountered.
  CyclicImport :: [ModuleName] -> DiscoError
  -- | Error encountered during typechecking.
  TypeCheckErr :: LocTCError -> DiscoError
  -- | Error encountered during parsing.
  ParseErr :: ParseErrorBundle String DiscoParseError -> DiscoError
  -- | Error encountered at runtime.
  EvalErr :: EvalError -> DiscoError
  -- | Something that shouldn't happen; indicates the presence of a
  --   bug.
  Panic :: String -> DiscoError
  deriving (Int -> DiscoError -> ShowS
[DiscoError] -> ShowS
DiscoError -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DiscoError] -> ShowS
$cshowList :: [DiscoError] -> ShowS
show :: DiscoError -> String
$cshow :: DiscoError -> String
showsPrec :: Int -> DiscoError -> ShowS
$cshowsPrec :: Int -> DiscoError -> ShowS
Show)

-- | Errors that can be generated at runtime.
data EvalError where
  -- | An unbound name was encountered.
  UnboundError :: QName core -> EvalError
  -- | An unbound name that really shouldn't happen, coming from some
  --   kind of internal name generation scheme.
  UnboundPanic :: Name core -> EvalError
  -- | Division by zero.
  DivByZero :: EvalError
  -- | Overflow, e.g. (2^66)!
  Overflow :: EvalError
  -- | Non-exhaustive case analysis.
  NonExhaustive :: EvalError
  -- | Infinite loop detected via black hole.
  InfiniteLoop :: EvalError
  -- | User-generated crash.
  Crash :: String -> EvalError

deriving instance Show EvalError

panic :: Member (Error DiscoError) r => String -> Sem r a
panic :: forall (r :: EffectRow) a.
Member (Error DiscoError) r =>
String -> Sem r a
panic = forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> DiscoError
Panic

outputDiscoErrors :: Member (Output (Message ann)) r => Sem (Error DiscoError ': r) () -> Sem r ()
outputDiscoErrors :: forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem (Error DiscoError : r) () -> Sem r ()
outputDiscoErrors Sem (Error DiscoError : r) ()
m = do
  Either DiscoError ()
e <- forall e (r :: EffectRow) a.
Sem (Error e : r) a -> Sem r (Either e a)
runError Sem (Error DiscoError : r) ()
m
  forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
err forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty') forall (m :: * -> *) a. Monad m => a -> m a
return Either DiscoError ()
e

instance Pretty DiscoError where
  pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
DiscoError -> Sem r (Doc ann)
pretty = \case
    ModuleNotFound String
m -> Sem r (Doc ann)
"Error: couldn't find a module named '" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
m forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"'."
    CyclicImport [ModuleName]
ms -> forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
[ModuleName] -> Sem r (Doc ann)
cyclicImportError [ModuleName]
ms
    TypeCheckErr (LocTCError Maybe (QName Term)
Nothing TCError
te) -> forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
TCError -> Sem r (Doc ann)
prettyTCError TCError
te
    TypeCheckErr (LocTCError (Just QName Term
n) TCError
te) ->
      forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
        [ Sem r (Doc ann)
"While checking " forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' QName Term
n forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
":"
        , forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
TCError -> Sem r (Doc ann)
prettyTCError TCError
te
        ]
    ParseErr ParseErrorBundle String DiscoParseError
pe -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
errorBundlePretty ParseErrorBundle String DiscoParseError
pe)
    EvalErr EvalError
ee -> forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
EvalError -> Sem r (Doc ann)
prettyEvalError EvalError
ee
    Panic String
s ->
      forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
        [ Sem r (Doc ann)
"Bug! " forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
s
        , Sem r (Doc ann)
"Please report this as a bug at https://github.com/disco-lang/disco/issues/ ."
        ]

rtd :: String -> Sem r (Doc ann)
rtd :: forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
page = Sem r (Doc ann)
"https://disco-lang.readthedocs.io/en/latest/reference/" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
page forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
".html"

issue :: Int -> Sem r (Doc ann)
issue :: forall (r :: EffectRow) ann. Int -> Sem r (Doc ann)
issue Int
n = Sem r (Doc ann)
"See https://github.com/disco-lang/disco/issues/" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (forall a. Show a => a -> String
show Int
n)

cyclicImportError ::
  Members '[Reader PA, LFresh] r =>
  [ModuleName] ->
  Sem r (Doc ann)
cyclicImportError :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
[ModuleName] -> Sem r (Doc ann)
cyclicImportError [ModuleName]
ms =
  forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
    [ Sem r (Doc ann)
"Error: module imports form a cycle:"
    , forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
" ->" (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [ModuleName]
ms)
    ]

prettyEvalError :: Members '[Reader PA, LFresh] r => EvalError -> Sem r (Doc ann)
prettyEvalError :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
EvalError -> Sem r (Doc ann)
prettyEvalError = \case
  UnboundPanic Name core
x ->
    (Sem r (Doc ann)
"Bug! No variable found named" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name core
x forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
".")
      forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ Sem r (Doc ann)
"Please report this as a bug at https://github.com/disco-lang/disco/issues/ ."
  UnboundError QName core
x -> Sem r (Doc ann)
"Error: encountered undefined name" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' QName core
x forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
". Maybe you haven't defined it yet?"
  EvalError
DivByZero -> Sem r (Doc ann)
"Error: division by zero."
  EvalError
Overflow -> Sem r (Doc ann)
"Error: that number would not even fit in the universe!"
  EvalError
NonExhaustive -> Sem r (Doc ann)
"Error: value did not match any of the branches in a case expression."
  EvalError
InfiniteLoop -> Sem r (Doc ann)
"Error: infinite loop detected!"
  Crash String
s -> Sem r (Doc ann)
"User crash:" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
s

-- [X] Step 1: nice error messages, make sure all are tested
-- [ ] Step 2: link to wiki/website with more info on errors!
-- [ ] Step 3: improve error messages according to notes below
-- [ ] Step 4: get it to return multiple error messages
-- [ ] Step 5: save parse locations, display with errors
prettyTCError :: Members '[Reader PA, LFresh] r => TCError -> Sem r (Doc ann)
prettyTCError :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
TCError -> Sem r (Doc ann)
prettyTCError = \case
  -- XXX include some potential misspellings along with Unbound
  --   see https://github.com/disco-lang/disco/issues/180
  Unbound Name Term
x ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: there is nothing named" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name Term
x forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"unbound"
      ]
  Ambiguous Name Term
x [ModuleName]
ms ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: the name" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name Term
x forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"is ambiguous. It could refer to:"
      , forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
indent Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\ModuleName
m -> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' ModuleName
m forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"." forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name Term
x) forall a b. (a -> b) -> a -> b
$ [ModuleName]
ms
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"ambiguous"
      ]
  NoType Name Term
x ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: the definition of" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name Term
x forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"must have an accompanying type signature."
      , Sem r (Doc ann)
"Try writing something like '"
          forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name Term
x
          forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
": Int' (or whatever the type of"
          forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name Term
x
          forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"should be) first."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"missingtype"
      ]
  NotCon Con
c Term
t Type
ty ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: the expression"
      , forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
indent Int
2 forall a b. (a -> b) -> a -> b
$ forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Term
t
      , Sem r (Doc ann)
"must have both a" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann. Con -> Sem r (Doc ann)
conWord Con
c forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"type and also the incompatible type"
      , forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
indent Int
2 forall a b. (a -> b) -> a -> b
$ forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Type
ty forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"notcon"
      ]
  TCError
EmptyCase ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: empty case expressions {? ?} are not allowed."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"empty-case"
      ]
  PatternType Con
c Pattern
pat Type
ty ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: the pattern"
      , forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
indent Int
2 forall a b. (a -> b) -> a -> b
$ forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Pattern
pat
      , Sem r (Doc ann)
"is supposed to have type"
      , forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
indent Int
2 forall a b. (a -> b) -> a -> b
$ forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Type
ty forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
","
      , Sem r (Doc ann)
"but instead it has a" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann. Con -> Sem r (Doc ann)
conWord Con
c forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"type."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"pattern-type"
      ]
  DuplicateDecls Name Term
x ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: duplicate type signature for" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name Term
x forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"dup-sig"
      ]
  DuplicateDefns Name Term
x ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: duplicate definition for" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name Term
x forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"dup-def"
      ]
  DuplicateTyDefns String
s ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: duplicate definition for type" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
s forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"dup-tydef"
      ]
  -- XXX include all types involved in the cycle.
  CyclicTyDef String
s ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: cyclic type definition for" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
s forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"cyc-ty"
      ]
  -- XXX lots more info!  & Split into several different errors.
  TCError
NumPatterns ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: number of arguments does not match."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"num-args"
      ]
  NonlinearPattern Pattern
p Name Term
x ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: pattern" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Pattern
p forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"contains duplicate variable" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name Term
x forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"nonlinear"
      ]
  NoSearch Type
ty ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: the type"
      , forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
indent Int
2 forall a b. (a -> b) -> a -> b
$ forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Type
ty
      , Sem r (Doc ann)
"is not searchable (i.e. it cannot be used in a forall)."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"no-search"
      ]
  Unsolvable SolveError
solveErr -> forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
SolveError -> Sem r (Doc ann)
prettySolveError SolveError
solveErr
  -- XXX maybe include close edit-distance alternatives?
  NotTyDef String
s ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: there is no built-in or user-defined type named '" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
s forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"'."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"no-tydef"
      ]
  TCError
NoTWild ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: wildcards (_) are not allowed in expressions."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"wildcard-expr"
      ]
  -- XXX say how many are expected, how many there were, what the actual arguments were?
  -- XXX distinguish between built-in and user-supplied type constructors in the error
  --     message?
  NotEnoughArgs Con
con ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: not enough arguments for the type '" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Con
con forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"'."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"num-args-type"
      ]
  TooManyArgs Con
con ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: too many arguments for the type '" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Con
con forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"'."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"num-args-type"
      ]
  -- XXX Mention the definition in which it was found, suggest adding the variable
  --     as a parameter
  UnboundTyVar Name Type
v ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: Unknown type variable '" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name Type
v forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"'."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"unbound-tyvar"
      ]
  NoPolyRec String
s [String]
ss [Type]
tys ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: in the definition of " forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
s forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text [String]
ss)) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
": recursive occurrences of" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
s forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"may only have type variables as arguments."
      , forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
indent
          Int
2
          ( forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
s forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' [Type]
tys)) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"does not follow this rule."
          )
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"no-poly-rec"
      ]
  TCError
NoError -> forall (m :: * -> *) ann. Applicative m => m (Doc ann)
empty

conWord :: Con -> Sem r (Doc ann)
conWord :: forall (r :: EffectRow) ann. Con -> Sem r (Doc ann)
conWord = \case
  Con
CArr -> Sem r (Doc ann)
"function"
  Con
CProd -> Sem r (Doc ann)
"pair"
  Con
CSum -> Sem r (Doc ann)
"sum"
  Con
CSet -> Sem r (Doc ann)
"set"
  Con
CBag -> Sem r (Doc ann)
"bag"
  Con
CList -> Sem r (Doc ann)
"list"
  CContainer Atom
_ -> Sem r (Doc ann)
"container"
  Con
CMap -> Sem r (Doc ann)
"map"
  Con
CGraph -> Sem r (Doc ann)
"graph"
  CUser String
s -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
s

prettySolveError :: Members '[Reader PA, LFresh] r => SolveError -> Sem r (Doc ann)
prettySolveError :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
SolveError -> Sem r (Doc ann)
prettySolveError = \case
  -- XXX say which types!
  SolveError
NoWeakUnifier ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: the shape of two types does not match."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"shape-mismatch"
      ]
  -- XXX say more!  XXX HIGHEST PRIORITY!
  SolveError
NoUnify ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: typechecking failed."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"typecheck-fail"
      ]
  UnqualBase Qualifier
q BaseTy
b ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: values of type" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' BaseTy
b forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann. Bool -> Qualifier -> Sem r (Doc ann)
qualPhrase Bool
False Qualifier
q forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"not-qual"
      ]
  Unqual Qualifier
q Type
ty ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: values of type" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Type
ty forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann. Bool -> Qualifier -> Sem r (Doc ann)
qualPhrase Bool
False Qualifier
q forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"not-qual"
      ]
  QualSkolem Qualifier
q Name Type
a ->
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ann)
"Error: type variable" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name Type
a forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"represents any type, so we cannot assume values of that type"
      , forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
indent Int
2 (forall (r :: EffectRow) ann. Bool -> Qualifier -> Sem r (Doc ann)
qualPhrase Bool
True Qualifier
q) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"."
      , forall (r :: EffectRow) ann. String -> Sem r (Doc ann)
rtd String
"qual-skolem"
      ]

qualPhrase :: Bool -> Qualifier -> Sem r (Doc ann)
qualPhrase :: forall (r :: EffectRow) ann. Bool -> Qualifier -> Sem r (Doc ann)
qualPhrase Bool
b Qualifier
q
  | Qualifier
q forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Qualifier
QBool, Qualifier
QBasic, Qualifier
QSimple] = Sem r (Doc ann)
"are" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> (if Bool
b then forall (m :: * -> *) ann. Applicative m => m (Doc ann)
empty else Sem r (Doc ann)
"not") forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann. Qualifier -> Sem r (Doc ann)
qualAction Qualifier
q
  | Bool
otherwise = Sem r (Doc ann)
"can" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> (if Bool
b then forall (m :: * -> *) ann. Applicative m => m (Doc ann)
empty else Sem r (Doc ann)
"not") forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"be" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann. Qualifier -> Sem r (Doc ann)
qualAction Qualifier
q

qualAction :: Qualifier -> Sem r (Doc ann)
qualAction :: forall (r :: EffectRow) ann. Qualifier -> Sem r (Doc ann)
qualAction = \case
  Qualifier
QNum -> Sem r (Doc ann)
"added and multiplied"
  Qualifier
QSub -> Sem r (Doc ann)
"subtracted"
  Qualifier
QDiv -> Sem r (Doc ann)
"divided"
  Qualifier
QCmp -> Sem r (Doc ann)
"compared"
  Qualifier
QEnum -> Sem r (Doc ann)
"enumerated"
  Qualifier
QBool -> Sem r (Doc ann)
"boolean"
  Qualifier
QBasic -> Sem r (Doc ann)
"basic"
  Qualifier
QSimple -> Sem r (Doc ann)
"simple"