unisonweb/unison
1
0
Fork 0
mirror of https://github.com/unisonweb/unison.git synced 2024-09-21 07:17:25 +03:00
Code Issues Projects Releases Wiki Activity

Track type variables in monadic pretty-printer

Browse Source
This commit is contained in:
Rúnar 2022-10-26 20:41:21 -04:00
parent 52f2632133
commit 2508f40232
12 changed files with 1046 additions and 919 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
codebase2/util/src/U/Util/Monoid.hs
View File

@ -1,6 +1,7 @@
module U.Util.Monoid where
import Control.Monad (foldM)
import Control.Monad.Extra ((>=>))
import Data.Foldable (toList)
import Data.List (intersperse)
@ -10,6 +11,9 @@ intercalateMap :: (Foldable t, Monoid a) => a -> (b -> a) -> t b -> a
intercalateMap separator renderer elements =
mconcat $ intersperse separator (renderer <$> toList elements)
intercalateMapM :: (Traversable t, Monad m, Monoid a) => a -> (b -> m a) -> t b -> m a
intercalateMapM separator renderer = traverse renderer >=> return . intercalateMap separator id
fromMaybe :: Monoid a => Maybe a -> a
fromMaybe Nothing = mempty
fromMaybe (Just a) = a
@ -24,4 +28,4 @@ isEmpty a = a == mempty
nonEmpty = not . isEmpty
foldMapM :: (Monad m, Foldable f, Monoid b) => (a -> m b) -> f a -> m b
foldMapM f as = foldM (\b a -> fmap (b <>) (f a)) mempty as
foldMapM f = foldM (\b a -> fmap (b <>) (f a)) mempty

4
lib/unison-pretty-printer/src/Unison/Util/Pretty.hs
View File

@ -102,6 +102,7 @@ module Unison.Util.Pretty
spaceIfNeeded,
spaced,
spacedMap,
spacedTraverse,
spacesIfBreak,
string,
surroundCommas,
@ -406,6 +407,9 @@ spaced = intercalateMap softbreak id
spacedMap :: (Foldable f, IsString s) => (a -> Pretty s) -> f a -> Pretty s
spacedMap f as = spaced . fmap f $ toList as
spacedTraverse :: (Traversable f, IsString s, Applicative m) => (a -> m (Pretty s)) -> f a -> m (Pretty s)
spacedTraverse f as = spaced <$> traverse f as
commas :: (Foldable f, IsString s) => f (Pretty s) -> Pretty s
commas = intercalateMap ("," <> softbreak) id

47
parser-typechecker/src/Unison/PrettyPrintEnv/MonadPretty.hs Normal file
View File

@ -0,0 +1,47 @@
{-# LANGUAGE ConstraintKinds #-}
module Unison.PrettyPrintEnv.MonadPretty where
import Control.Lens (over, set, view, views, _1, _2)
import Control.Monad.Reader (MonadReader, Reader, local, runReader)
import qualified Data.Set as Set
import Unison.Prelude (Set)
import Unison.PrettyPrintEnv (PrettyPrintEnv)
import Unison.Var (Var)
type MonadPretty v m = (Var v, MonadReader (PrettyPrintEnv, Set v) m)
getPPE :: MonadPretty v m => m PrettyPrintEnv
getPPE = view _1
-- | Run a computation with a modified PrettyPrintEnv, restoring the original
withPPE :: MonadPretty v m => PrettyPrintEnv -> m a -> m a
withPPE p = local (set _1 p)
applyPPE :: MonadPretty v m => (PrettyPrintEnv -> a) -> m a
applyPPE = views _1
applyPPE2 :: MonadPretty v m => (PrettyPrintEnv -> a -> b) -> a -> m b
applyPPE2 f a = views _1 (`f` a)
applyPPE3 :: MonadPretty v m => (PrettyPrintEnv -> a -> b -> c) -> a -> b -> m c
applyPPE3 f a b = views _1 (\ppe -> f ppe a b)
-- | Run a computation with a modified PrettyPrintEnv, restoring the original
modifyPPE :: MonadPretty v m => (PrettyPrintEnv -> PrettyPrintEnv) -> m a -> m a
modifyPPE = local . over _1
modifyTypeVars :: MonadPretty v m => (Set v -> Set v) -> m a -> m a
modifyTypeVars = local . over _2
-- | Add type variables to the set of variables that need to be avoided
addTypeVars :: MonadPretty v m => [v] -> m a -> m a
addTypeVars = modifyTypeVars . Set.union . Set.fromList
-- | Check if a list of type variables contains any variables that need to be
-- avoided
willCapture :: MonadPretty v m => [v] -> m Bool
willCapture vs = views _2 (not . Set.null . Set.intersection (Set.fromList vs))
runPretty :: Var v => PrettyPrintEnv -> Reader (PrettyPrintEnv, Set v) a -> a
runPretty ppe m = runReader m (ppe, mempty)

23
parser-typechecker/src/Unison/Syntax/DeclPrinter.hs
View File

@ -17,6 +17,7 @@ import qualified Unison.Name as Name
import Unison.Prelude
import Unison.PrettyPrintEnv (PrettyPrintEnv)
import qualified Unison.PrettyPrintEnv as PPE
import Unison.PrettyPrintEnv.MonadPretty (runPretty)
import Unison.PrettyPrintEnvDecl (PrettyPrintEnvDecl (..))
import Unison.Reference (Reference (DerivedId))
import qualified Unison.Referent as Referent
@ -73,9 +74,9 @@ prettyGADT env ctorType r name dd =
where
constructor (n, (_, _, t)) =
prettyPattern env ctorType name (ConstructorReference r n)
<> (fmt S.TypeAscriptionColon " :")
`P.hang` TypePrinter.pretty0 env Map.empty (-1) t
header = prettyEffectHeader name (DD.EffectDeclaration dd) <> (fmt S.ControlKeyword " where")
<> fmt S.TypeAscriptionColon " :"
`P.hang` TypePrinter.prettySyntax env t
header = prettyEffectHeader name (DD.EffectDeclaration dd) <> fmt S.ControlKeyword " where"
prettyPattern ::
PrettyPrintEnv ->
@ -86,7 +87,7 @@ prettyPattern ::
prettyPattern env ctorType namespace ref =
styleHashQualified''
(fmt (S.TermReference conRef))
( HQ.stripNamespace (fromMaybe "" $ Name.toText <$> HQ.toName namespace) $
( HQ.stripNamespace (maybe "" Name.toText (HQ.toName namespace)) $
PPE.termName env conRef
)
where
@ -106,26 +107,26 @@ prettyDataDecl (PrettyPrintEnvDecl unsuffixifiedPPE suffixifiedPPE) r name dd =
[0 ..]
(DD.constructors' dd)
where
constructor (n, (_, _, (Type.ForallsNamed' _ t))) = constructor' n t
constructor (n, (_, _, Type.ForallsNamed' _ t)) = constructor' n t
constructor (n, (_, _, t)) = constructor' n t
constructor' n t = case Type.unArrows t of
Nothing -> prettyPattern suffixifiedPPE CT.Data name (ConstructorReference r n)
Just ts -> case fieldNames unsuffixifiedPPE r name dd of
Nothing ->
P.group . P.hang' (prettyPattern suffixifiedPPE CT.Data name (ConstructorReference r n)) " " $
P.spaced (TypePrinter.prettyRaw suffixifiedPPE Map.empty 10 <$> init ts)
P.spaced (runPretty suffixifiedPPE (traverse (TypePrinter.prettyRaw Map.empty 10) (init ts)))
Just fs ->
P.group $
(fmt S.DelimiterChar "{ ")
fmt S.DelimiterChar "{ "
<> P.sep
((fmt S.DelimiterChar ",") <> " " `P.orElse` "\n ")
(fmt S.DelimiterChar "," <> " " `P.orElse` "\n ")
(field <$> zip fs (init ts))
<> (fmt S.DelimiterChar " }")
<> fmt S.DelimiterChar " }"
field (fname, typ) =
P.group $
styleHashQualified'' (fmt (S.TypeReference r)) fname
<> (fmt S.TypeAscriptionColon " :") `P.hang` TypePrinter.prettyRaw suffixifiedPPE Map.empty (-1) typ
header = prettyDataHeader name dd <> (fmt S.DelimiterChar (" = " `P.orElse` "\n = "))
<> fmt S.TypeAscriptionColon " :" `P.hang` runPretty suffixifiedPPE (TypePrinter.prettyRaw Map.empty (-1) typ)
header = prettyDataHeader name dd <> fmt S.DelimiterChar (" = " `P.orElse` "\n = ")
-- Comes up with field names for a data declaration which has the form of a
-- record, like `type Pt = { x : Int, y : Int }`. Works by generating the

1108
parser-typechecker/src/Unison/Syntax/TermPrinter.hs
View File

File diff suppressed because it is too large Load Diff

220
parser-typechecker/src/Unison/Syntax/TypePrinter.hs
View File

@ -1,5 +1,6 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Unison.Syntax.TypePrinter
( pretty,
@ -23,6 +24,7 @@ import Unison.Prelude
import Unison.PrettyPrintEnv (PrettyPrintEnv)
import qualified Unison.PrettyPrintEnv as PrettyPrintEnv
import Unison.PrettyPrintEnv.FQN (Imports, elideFQN)
import Unison.PrettyPrintEnv.MonadPretty (MonadPretty, getPPE, runPretty, willCapture)
import Unison.Reference (Reference, pattern Builtin)
import Unison.Referent (Referent)
import Unison.Syntax.NamePrinter (styleHashQualified'')
@ -36,17 +38,17 @@ import qualified Unison.Var as Var
type SyntaxText = S.SyntaxText' Reference
pretty :: forall v a. (Var v) => PrettyPrintEnv -> Type v a -> Pretty ColorText
pretty ppe = PP.syntaxToColor . prettySyntax ppe
pretty :: Var v => PrettyPrintEnv -> Type v a -> Pretty ColorText
pretty ppe t = PP.syntaxToColor $ prettySyntax ppe t
prettySyntax :: forall v a. (Var v) => PrettyPrintEnv -> Type v a -> Pretty SyntaxText
prettySyntax ppe = pretty0 ppe mempty (-1)
prettySyntax :: Var v => PrettyPrintEnv -> Type v a -> Pretty SyntaxText
prettySyntax ppe = runPretty ppe . pretty0 Map.empty (-1)
prettyStr :: Var v => Maybe Width -> PrettyPrintEnv -> Type v a -> String
prettyStr (Just width) n t =
toPlain $ PP.render width $ PP.syntaxToColor $ pretty0 n Map.empty (-1) t
prettyStr Nothing n t =
toPlain $ PP.render maxBound $ PP.syntaxToColor $ pretty0 n Map.empty (-1) t
prettyStr (Just width) ppe t =
toPlain . PP.render width . PP.syntaxToColor . runPretty ppe $ pretty0 Map.empty (-1) t
prettyStr Nothing ppe t =
toPlain . PP.render maxBound . PP.syntaxToColor . runPretty ppe $ pretty0 Map.empty (-1) t
{- Explanation of precedence handling
@ -71,90 +73,103 @@ prettyStr Nothing n t =
-}
pretty0 ::
forall v a.
(Var v) =>
PrettyPrintEnv ->
forall v a m.
MonadPretty v m =>
Imports ->
Int ->
Type v a ->
Pretty SyntaxText
pretty0 n im p tp = prettyRaw n im p (cleanup (removePureEffects tp))
m (Pretty SyntaxText)
pretty0 im p tp = prettyRaw im p (cleanup (removePureEffects tp))
prettyRaw ::
forall v a.
(Var v) =>
PrettyPrintEnv ->
forall v a m.
MonadPretty v m =>
Imports ->
Int ->
Type v a ->
Pretty SyntaxText
m (Pretty SyntaxText)
-- p is the operator precedence of the enclosing context (a number from 0 to
-- 11, or -1 to avoid outer parentheses unconditionally). Function
-- application has precedence 10.
prettyRaw n im p tp = go n im p tp
prettyRaw im p tp = go im p tp
where
go :: PrettyPrintEnv -> Imports -> Int -> Type v a -> Pretty SyntaxText
go n im p tp = case stripIntroOuters tp of
Var' v -> fmt S.Var $ PP.text (Var.name v)
DD.TupleType' xs | length xs /= 1 -> PP.parenthesizeCommas $ map (go n im 0) xs
go :: Imports -> Int -> Type v a -> m (Pretty SyntaxText)
go im p tp = case stripIntroOuters tp of
Var' v -> pure . fmt S.Var $ PP.text (Var.name v)
DD.TupleType' xs | length xs /= 1 -> PP.parenthesizeCommas <$> traverse (go im 0) xs
-- Would be nice to use a different SyntaxHighlights color if the reference is an ability.
Ref' r -> styleHashQualified'' (fmt $ S.TypeReference r) $ elideFQN im (PrettyPrintEnv.typeName n r)
Cycle' _ _ -> fromString "error: TypeParser does not currently emit Cycle"
Abs' _ -> fromString "error: TypeParser does not currently emit Abs"
Ann' _ _ -> fromString "error: TypeParser does not currently emit Ann"
App' (Ref' (Builtin "Sequence")) x ->
PP.group $ (fmt S.DelimiterChar "[") <> go n im (-1) x <> (fmt S.DelimiterChar "]")
Ref' r -> do
n <- getPPE
pure $ styleHashQualified'' (fmt $ S.TypeReference r) $ elideFQN im (PrettyPrintEnv.typeName n r)
Cycle' _ _ -> pure $ fromString "bug: TypeParser does not currently emit Cycle"
Abs' _ -> pure $ fromString "bug: TypeParser does not currently emit Abs"
Ann' _ _ -> pure $ fromString "bug: TypeParser does not currently emit Ann"
App' (Ref' (Builtin "Sequence")) x -> do
x' <- go im (-1) x
pure $ PP.group $ fmt S.DelimiterChar "[" <> x' <> fmt S.DelimiterChar "]"
Apps' f xs ->
PP.parenthesizeIf (p >= 10) $
go n im 9 f
`PP.hang` PP.spaced
(go n im 10 <$> xs)
PP.parenthesizeIf (p >= 10)
<$> ( PP.hang <$> go im 9 f <*> (PP.spaced <$> traverse (go im 10) xs)
)
Effect1' e t ->
PP.parenthesizeIf (p >= 10) $ go n im 9 e <> " " <> go n im 10 t
PP.parenthesizeIf (p >= 10) <$> ((\x y -> x <> " " <> y) <$> go im 9 e <*> go im 10 t)
Effects' es -> effects (Just es)
ForallsNamed' vs' body ->
let vs = filter (\v -> Var.name v /= "()") vs'
in if p < 0 && all Var.universallyQuantifyIfFree vs
then go n im p body
else
paren (p >= 0) $
let vformatted = PP.sep " " (fmt S.Var . PP.text . Var.name <$> vs)
in (fmt S.TypeOperator "∀ " <> vformatted <> fmt S.TypeOperator ".")
`PP.hang` go n im (-1) body
prettyForall p = do
let vformatted = PP.sep " " (fmt S.Var . PP.text . Var.name <$> vs)
PP.hang (fmt S.TypeOperator "∀ " <> vformatted <> fmt S.TypeOperator ".") <$> go im p body
in -- if we're printing a type signature, and all the type variables
-- are universally quantified, then we can omit the `forall` keyword
-- only if the type variables are not bound in an outer scope
if p < 0 && all Var.universallyQuantifyIfFree vs
then ifM (willCapture vs) (prettyForall p) (go im p body)
else paren (p >= 0) <$> prettyForall (-1)
t@(Arrow' _ _) -> case t of
EffectfulArrows' (Ref' DD.UnitRef) rest ->
PP.parenthesizeIf (p >= 10) $ arrows True True rest
PP.parenthesizeIf (p >= 10) <$> arrows True True rest
EffectfulArrows' fst rest ->
case fst of
Var' v
| Var.name v == "()" ->
PP.parenthesizeIf (p >= 10) $ arrows True True rest
PP.parenthesizeIf (p >= 10) <$> arrows True True rest
_ ->
PP.parenthesizeIf (p >= 0) $
go n im 0 fst <> arrows False False rest
_ -> "error"
_ -> "error"
effects Nothing = mempty
effects (Just es) = PP.group $ fmt S.AbilityBraces "{" <> PP.commas (go n im 0 <$> es) <> (fmt S.AbilityBraces "}")
PP.parenthesizeIf (p >= 0)
<$> ((<>) <$> go im 0 fst <*> arrows False False rest)
_ -> pure . fromString $ "bug: unexpected Arrow form in prettyRaw: " <> show t
_ -> pure . fromString $ "bug: unexpected form in prettyRaw: " <> show tp
effects Nothing = pure mempty
effects (Just es) =
PP.group . (fmt S.AbilityBraces "{" <>) . (<> fmt S.AbilityBraces "}")
<$> (PP.commas <$> traverse (go im 0) es)
-- `first`: is this the first argument?
-- `mes`: list of effects
arrow delay first mes =
(if first then mempty else PP.softbreak <> fmt S.TypeOperator "->")
<> (if delay then (if first then fmt S.DelayForceChar "'" else fmt S.DelayForceChar " '") else mempty)
<> effects mes
<> if isJust mes || not delay && not first then " " else mempty
arrow delay first mes = do
es <- effects mes
pure $
(if first then mempty else PP.softbreak <> fmt S.TypeOperator "->")
<> (if delay then (if first then fmt S.DelayForceChar "'" else fmt S.DelayForceChar " '") else mempty)
<> es
<> if isJust mes || not delay && not first then " " else mempty
arrows delay first [(mes, Ref' DD.UnitRef)] = arrow delay first mes <> fmt S.Unit "()"
arrows delay first ((mes, Ref' DD.UnitRef) : rest) =
arrow delay first mes <> parenNoGroup delay (arrows True True rest)
arrows delay first ((mes, arg) : rest) =
arrow delay first mes
<> parenNoGroup
(delay && not (null rest))
(go n im 0 arg <> arrows False False rest)
arrows False False [] = mempty
arrows False True [] = mempty -- not reachable
arrows True _ [] = mempty -- not reachable
arrows ::
Bool ->
Bool ->
[(Maybe [Type v a], Type v a)] ->
m (Pretty SyntaxText)
arrows delay first [(mes, Ref' DD.UnitRef)] = (<> fmt S.Unit "()") <$> arrow delay first mes
arrows delay first ((mes, Ref' DD.UnitRef) : rest) = do
es <- arrow delay first mes
rest' <- arrows True True rest
pure $ es <> parenNoGroup delay rest'
arrows delay first ((mes, arg) : rest) = do
es <- arrow delay first mes
arg' <- go im 0 arg
rest' <- arrows False False rest
pure $ es <> parenNoGroup (delay && not (null rest)) (arg' <> rest')
arrows False False [] = pure mempty
arrows False True [] = pure mempty -- not reachable
arrows True _ [] = pure mempty -- not reachable
paren True s = PP.group $ fmt S.Parenthesis "(" <> s <> fmt S.Parenthesis ")"
paren False s = PP.group s
@ -166,61 +181,62 @@ fmt = PP.withSyntax
-- todo: provide sample output in comment
prettySignaturesCT ::
Var v =>
PrettyPrintEnv ->
MonadPretty v m =>
[(Referent, HashQualified Name, Type v a)] ->
[Pretty ColorText]
prettySignaturesCT env ts = map PP.syntaxToColor $ prettySignaturesST env ts
m [Pretty ColorText]
prettySignaturesCT ts = map PP.syntaxToColor <$> prettySignaturesST ts
prettySignaturesCTCollapsed ::
Var v =>
PrettyPrintEnv ->
MonadPretty v m =>
[(Referent, HashQualified Name, Type v a)] ->
Pretty ColorText
prettySignaturesCTCollapsed env ts =
PP.lines $
PP.group <$> prettySignaturesCT env ts
m (Pretty ColorText)
prettySignaturesCTCollapsed ts =
PP.lines
. map PP.group
<$> prettySignaturesCT ts
prettySignaturesST ::
Var v =>
PrettyPrintEnv ->
MonadPretty v m =>
[(Referent, HashQualified Name, Type v a)] ->
[Pretty SyntaxText]
prettySignaturesST env ts =
PP.align [(name r hq, sig typ) | (r, hq, typ) <- ts]
m [Pretty SyntaxText]
prettySignaturesST ts =
PP.align <$> traverse (\(r, hq, typ) -> (name r hq,) <$> sig typ) ts
where
name r hq =
styleHashQualified'' (fmt $ S.TermReference r) hq
sig typ =
(fmt S.TypeAscriptionColon ": " <> pretty0 env Map.empty (-1) typ)
`PP.orElse` (fmt S.TypeAscriptionColon ": " <> PP.indentNAfterNewline 2 (pretty0 env Map.empty (-1) typ))
sig typ = do
t <- pretty0 Map.empty (-1) typ
let col = fmt S.TypeAscriptionColon ": "
pure $ (col <> t) `PP.orElse` (col <> PP.indentNAfterNewline 2 t)
-- todo: provide sample output in comment; different from prettySignatures'
prettySignaturesAlt' ::
Var v =>
PrettyPrintEnv ->
forall a v m.
MonadPretty v m =>
[([HashQualified Name], Type v a)] ->
[Pretty ColorText]
prettySignaturesAlt' env ts =
map PP.syntaxToColor $
PP.align
[ ( PP.commas . fmap (\name -> styleHashQualified'' (fmt $ S.HashQualifier name) name) $ names,
(fmt S.TypeAscriptionColon ": " <> pretty0 env Map.empty (-1) typ)
`PP.orElse` ( fmt S.TypeAscriptionColon ": "
<> PP.indentNAfterNewline 2 (pretty0 env Map.empty (-1) typ)
)
m [Pretty ColorText]
prettySignaturesAlt' ts =
do
ts' <- traverse f ts
pure $ map PP.syntaxToColor $ PP.align ts'
where
f :: ([HashQualified Name], Type v a) -> m (Pretty SyntaxText, Pretty SyntaxText)
f (names, typ) = do
typ' <- pretty0 Map.empty (-1) typ
let col = fmt S.TypeAscriptionColon ": "
pure
( PP.commas . fmap (\name -> styleHashQualified'' (fmt $ S.HashQualifier name) name) $ names,
(col <> typ') `PP.orElse` (col <> PP.indentNAfterNewline 2 typ')
)
| (names, typ) <- ts
]
-- prettySignatures'' :: Var v => PrettyPrintEnv -> [(Name, Type v a)] -> [Pretty ColorText]
-- prettySignatures'' :: Var v => [(Name, Type v a)] -> [Pretty ColorText]
-- prettySignatures'' env ts = prettySignatures' env (first HQ.fromName <$> ts)
prettySignaturesAlt ::
Var v =>
PrettyPrintEnv ->
MonadPretty v m =>
[([HashQualified Name], Type v a)] ->
Pretty ColorText
prettySignaturesAlt env ts =
PP.lines $
PP.group <$> prettySignaturesAlt' env ts
m (Pretty ColorText)
prettySignaturesAlt ts =
PP.lines
. map PP.group
<$> prettySignaturesAlt' ts

415
parser-typechecker/src/Unison/Typechecker/Context.hs
View File

@ -326,13 +326,13 @@ removeSyntheticTypeVars typ =
go v
| Var.User _ <- Var.typeOf v = pure v -- user-provided type variables left alone
| otherwise = do
(used, curMappings) <- get
case Map.lookup v curMappings of
Nothing -> do
let v' = pickName used (Var.typeOf v)
put (Set.insert v' used, Map.insert v v' curMappings)
pure v'
Just v' -> pure v'
(used, curMappings) <- get
case Map.lookup v curMappings of
Nothing -> do
let v' = pickName used (Var.typeOf v)
put (Set.insert v' used, Map.insert v v' curMappings)
pure v'
Just v' -> pure v'
pickName used vt = ABT.freshIn used . Var.named $ case vt of
-- for each type of variable, we have some preferred variable
-- names that we like, if they aren't already being used
@ -671,21 +671,21 @@ extend' e c@(Context ctx) = Context . (: ctx) . (e,) <$> i'
| Set.member v vs -> crash $ "variable " <> show v <> " already defined in the context"
| not (wellformedType c t) -> crash $ "type " <> show t <> " is not well-formed wrt the context"
| otherwise ->
pure $
Info (Set.insert v es) (Map.insert v sa ses) us uas (Set.insert v vs) pvs
pure $
Info (Set.insert v es) (Map.insert v sa ses) us uas (Set.insert v vs) pvs
-- VarCtx - ensure `v` is fresh, and annotation is well-formed wrt the context
Ann v t
| Set.member v vs -> crash $ "variable " <> show v <> " already defined in the context"
| not (wellformedType c t) -> crash $ "type " <> show t <> " is not well-formed wrt the context"
| otherwise ->
pure $
Info
es
ses
us
(Map.insert v t uas)
(Set.insert v vs)
((if Set.null (Type.freeVars t) then Set.insert v else id) pvs)
pure $
Info
es
ses
us
(Map.insert v t uas)
(Set.insert v vs)
((if Set.null (Type.freeVars t) then Set.insert v else id) pvs)
-- MarkerCtx - note that since a Marker is always the first mention of a variable, suffices to
-- just check that `v` is not previously mentioned
Marker v ->
@ -874,7 +874,7 @@ synthesizeApp ::
M v loc (Type v loc, Wanted v loc)
synthesizeApp _ ft arg
| debugEnabled && traceShow ("synthesizeApp" :: String, ft, arg) False =
undefined
undefined
synthesizeApp fun (Type.stripIntroOuters -> Type.Effect'' es ft) argp@(arg, argNum) =
scope (InSynthesizeApp ft arg argNum) $ do
(t, w) <- go ft
@ -1051,10 +1051,10 @@ synthesizeWanted (Term.Ann' (Term.Ref' _) t)
--
-- Top level references don't have their own effects.
| Set.null s = do
t <- existentializeArrows t
-- See note about ungeneralizing above in the Var case.
t <- ungeneralize t
pure (discard t, [])
t <- existentializeArrows t
-- See note about ungeneralizing above in the Var case.
t <- ungeneralize t
pure (discard t, [])
| otherwise = compilerCrash $ FreeVarsInTypeAnnotation s
where
s = ABT.freeVars t
@ -1158,59 +1158,59 @@ synthesizeWanted e
| Term.TermLink' _ <- e = pure (Type.termLink l, [])
| Term.TypeLink' _ <- e = pure (Type.typeLink l, [])
| Term.Blank' blank <- e = do
v <- freshenVar Var.blank
appendContext [Var (TypeVar.Existential blank v)]
pure (existential' l blank v, [])
v <- freshenVar Var.blank
appendContext [Var (TypeVar.Existential blank v)]
pure (existential' l blank v, [])
| Term.List' v <- e = do
ft <- vectorConstructorOfArity l (Foldable.length v)
case Foldable.toList v of
[] -> pure (ft, [])
v1 : _ ->
scope (InVectorApp (ABT.annotation v1)) $
synthesizeApps e ft v
ft <- vectorConstructorOfArity l (Foldable.length v)
case Foldable.toList v of
[] -> pure (ft, [])
v1 : _ ->
scope (InVectorApp (ABT.annotation v1)) $
synthesizeApps e ft v
-- ->I=> (Full Damas Milner rule)
| Term.Lam' body <- e = do
-- arya: are there more meaningful locations we could put into and
-- pull out of the abschain?)
[arg, i, e, o] <-
sequence
[ ABT.freshen body freshenVar,
freshenVar (ABT.variable body),
freshenVar Var.inferAbility,
freshenVar Var.inferOutput
]
let it = existential' l B.Blank i
ot = existential' l B.Blank o
et = existential' l B.Blank e
appendContext $
[existential i, existential e, existential o, Ann arg it]
body' <- pure $ ABT.bindInheritAnnotation body (Term.var () arg)
if Term.isLam body'
then checkWithAbilities [] body' ot
else checkWithAbilities [et] body' ot
ctx <- getContext
let t = apply ctx $ Type.arrow l it (Type.effect l [et] ot)
pure (t, [])
-- arya: are there more meaningful locations we could put into and
-- pull out of the abschain?)
[arg, i, e, o] <-
sequence
[ ABT.freshen body freshenVar,
freshenVar (ABT.variable body),
freshenVar Var.inferAbility,
freshenVar Var.inferOutput
]
let it = existential' l B.Blank i
ot = existential' l B.Blank o
et = existential' l B.Blank e
appendContext $
[existential i, existential e, existential o, Ann arg it]
body' <- pure $ ABT.bindInheritAnnotation body (Term.var () arg)
if Term.isLam body'
then checkWithAbilities [] body' ot
else checkWithAbilities [et] body' ot
ctx <- getContext
let t = apply ctx $ Type.arrow l it (Type.effect l [et] ot)
pure (t, [])
| Term.If' cond t f <- e = do
cwant <- scope InIfCond $ check cond (Type.boolean l)
(ty, bwant) <-
scope (InIfBody $ ABT.annotation t) $
synthesizeApps e (Type.iff2 l) [t, f]
(ty,) <$> coalesceWanted bwant cwant
cwant <- scope InIfCond $ check cond (Type.boolean l)
(ty, bwant) <-
scope (InIfBody $ ABT.annotation t) $
synthesizeApps e (Type.iff2 l) [t, f]
(ty,) <$> coalesceWanted bwant cwant
| Term.And' a b <- e =
scope InAndApp $ synthesizeApps e (Type.andor' l) [a, b]
scope InAndApp $ synthesizeApps e (Type.andor' l) [a, b]
| Term.Or' a b <- e =
scope InOrApp $ synthesizeApps e (Type.andor' l) [a, b]
scope InOrApp $ synthesizeApps e (Type.andor' l) [a, b]
| Term.Match' scrutinee cases <- e = do
(scrutineeType, swant) <- synthesize scrutinee
outputTypev <- freshenVar (Var.named "match-output")
let outputType = existential' l B.Blank outputTypev
appendContext [existential outputTypev]
cwant <- checkCases scrutineeType outputType cases
want <- coalesceWanted cwant swant
ctx <- getContext
pure $ (apply ctx outputType, want)
(scrutineeType, swant) <- synthesize scrutinee
outputTypev <- freshenVar (Var.named "match-output")
let outputType = existential' l B.Blank outputTypev
appendContext [existential outputTypev]
cwant <- checkCases scrutineeType outputType cases
want <- coalesceWanted cwant swant
ctx <- getContext
pure $ (apply ctx outputType, want)
where
l = loc e
synthesizeWanted _e = compilerCrash PatternMatchFailure
@ -1427,17 +1427,17 @@ checkPattern scrutineeType p =
-- 'otherwise' still needs to be covered for exhaustivity, however.
| Type.Apps' (Type.Ref' req) [_, r] <- scrutineeType,
req == Type.effectRef ->
checkPattern r p
checkPattern r p
| otherwise -> do
vt <- lift $ do
v <- freshenVar Var.inferPatternPureV
e <- freshenVar Var.inferPatternPureE
let vt = existentialp loc v
let et = existentialp loc e
appendContext [existential v, existential e]
subtype (Type.effectV loc (loc, et) (loc, vt)) scrutineeType
applyM vt
checkPattern vt p
vt <- lift $ do
v <- freshenVar Var.inferPatternPureV
e <- freshenVar Var.inferPatternPureE
let vt = existentialp loc v
let et = existentialp loc e
appendContext [existential v, existential e]
subtype (Type.effectV loc (loc, et) (loc, vt)) scrutineeType
applyM vt
checkPattern vt p
-- ex: { Stream.emit x -> k } -> ...
Pattern.EffectBind loc ref args k -> do
-- scrutineeType should be a supertype of `Effect e vt`
@ -1460,15 +1460,15 @@ checkPattern scrutineeType p =
Type.Effect'' [et] it
-- expecting scrutineeType to be `Effect et vt`
| Type.Apps' _ [eff, vt] <- st -> do
-- ensure that the variables in `et` unify with those from
-- the scrutinee.
lift $ abilityCheck' [eff] [et]
let kt =
Type.arrow
(Pattern.loc k)
it
(Type.effect (Pattern.loc k) [eff] vt)
(vs ++) <$> checkPattern kt k
-- ensure that the variables in `et` unify with those from
-- the scrutinee.
lift $ abilityCheck' [eff] [et]
let kt =
Type.arrow
(Pattern.loc k)
it
(Type.effect (Pattern.loc k) [eff] vt)
(vs ++) <$> checkPattern kt k
| otherwise -> lift . compilerCrash $ PatternMatchFailure
_ ->
lift . compilerCrash $
@ -1646,12 +1646,12 @@ tweakEffects ::
M v loc ([v], Type v loc)
tweakEffects v0 t0
| isEffectVar v0 t0 && isVariant v0 t0 =
rewrite (Just False) t0 >>= \case
([], ty) ->
freshenTypeVar v0 >>= \out -> finish [out] ty
(vs, ty) -> finish vs ty
rewrite (Just False) t0 >>= \case
([], ty) ->
freshenTypeVar v0 >>= \out -> finish [out] ty
(vs, ty) -> finish vs ty
| otherwise =
freshenTypeVar v0 >>= \out -> finish [out] t0
freshenTypeVar v0 >>= \out -> finish [out] t0
where
negative = fromMaybe False
@ -1665,27 +1665,27 @@ tweakEffects v0 t0
rewrite p ty
| Type.ForallNamed' v t <- ty,
v0 /= v =
second (Type.forall a v) <$> rewrite p t
second (Type.forall a v) <$> rewrite p t
| Type.Arrow' i o <- ty = do
(vis, i) <- rewrite (not <$> p) i
(vos, o) <- rewrite p o
pure (vis ++ vos, Type.arrow a i o)
(vis, i) <- rewrite (not <$> p) i
(vos, o) <- rewrite p o
pure (vis ++ vos, Type.arrow a i o)
| Type.Effect1' e t <- ty = do
(ves, e) <- rewrite p e
(vts, t) <- rewrite p t
pure (ves ++ vts, Type.effect1 a e t)
(ves, e) <- rewrite p e
(vts, t) <- rewrite p t
pure (ves ++ vts, Type.effect1 a e t)
| Type.Effects' es <- ty = do
ess <- traverse (rewrite p) es
let es = snd <$> ess; ves = fst =<< ess
pure (ves, Type.effects a es)
ess <- traverse (rewrite p) es
let es = snd <$> ess; ves = fst =<< ess
pure (ves, Type.effects a es)
| Type.Var' v <- ty,
v0 == v && negative p = do
u <- freshenTypeVar v0
pure ([u], existential' (loc ty) B.Blank u)
u <- freshenTypeVar v0
pure ([u], existential' (loc ty) B.Blank u)
| Type.App' f x <- ty = do
(vfs, f) <- rewrite p f
(vxs, x) <- rewrite Nothing x
pure (vfs ++ vxs, Type.app (loc ty) f x)
(vfs, f) <- rewrite p f
(vxs, x) <- rewrite Nothing x
pure (vfs ++ vxs, Type.app (loc ty) f x)
| otherwise = pure ([], ty)
where
a = loc ty
@ -1759,7 +1759,7 @@ generalizeExistentials ctx ty0 = generalizeP pred ctx ty
pred e
| pe@(Just (tv, _)) <- existentialP e,
tv `Set.member` fvs =
pe
pe
| otherwise = Nothing
generalizeP ::
@ -1775,13 +1775,13 @@ generalizeP p ctx0 ty = foldr gen (applyCtx ctx0 ty) ctx
gen (tv, v) t
| tv `ABT.isFreeIn` t =
-- location of the forall is just the location of the input type
-- and the location of each quantified variable is just inherited
-- from its source location
Type.forall
(loc t)
(TypeVar.Universal v)
(ABT.substInheritAnnotation tv (universal' () v) t)
-- location of the forall is just the location of the input type
-- and the location of each quantified variable is just inherited
-- from its source location
Type.forall
(loc t)
(TypeVar.Universal v)
(ABT.substInheritAnnotation tv (universal' () v) t)
-- don't bother introducing a forall if type variable is unused
| otherwise = t
@ -1867,20 +1867,20 @@ coalesceWanted' ::
coalesceWanted' _ [] old = pure old
coalesceWanted' keep ((loc, n) : new) old
| Just (_, o) <- find (headMatch n . snd) old = do
equate n o
coalesceWanted new old
equate n o
coalesceWanted new old
| Type.Var' u <- n = do
(new, old) <-
-- Only add existential variables to the wanted list if they
-- occur in a type we're trying to infer in the context. If
-- they don't, they were added as instantiations of polymorphic
-- types that might as well just be instantiated to {}.
if keep u
then pure (new, (loc, n) : old)
else do
defaultAbility n
pure (new, old)
coalesceWanted new old
(new, old) <-
-- Only add existential variables to the wanted list if they
-- occur in a type we're trying to infer in the context. If
-- they don't, they were added as instantiations of polymorphic
-- types that might as well just be instantiated to {}.
if keep u
then pure (new, (loc, n) : old)
else do
defaultAbility n
pure (new, old)
coalesceWanted new old
| otherwise = coalesceWanted' keep new ((loc, n) : old)
-- Wrapper for coalesceWanted' that ensures both lists are fully
@ -1922,10 +1922,10 @@ pruneWanted ::
pruneWanted acc [] _ = pure acc
pruneWanted acc ((loc, w) : want) handled
| Just h <- find (headMatch w) handled = do
subtype w h
want <- expandWanted want
handled <- expandAbilities handled
pruneWanted acc want handled
subtype w h
want <- expandWanted want
handled <- expandAbilities handled
pruneWanted acc want handled
| otherwise = pruneWanted ((loc, w) : acc) want handled
-- | Processes wanted effects with respect to a portion of context
@ -1947,7 +1947,7 @@ substAndDefaultWanted want ctx
| want <- (fmap . fmap) (applyCtx ctx) want,
want <- filter q want,
repush <- filter keep ctx =
appendContext repush *> coalesceWanted want []
appendContext repush *> coalesceWanted want []
where
isExistential TypeVar.Existential {} = True
isExistential _ = False
@ -2064,14 +2064,14 @@ relax t = relax' True v t
relax' :: Var v => Ord loc => Bool -> v -> Type v loc -> Type v loc
relax' nonArrow v t
| Type.Arrow' i o <- t =
Type.arrow (ABT.annotation t) i $ relax' nonArrow v o
Type.arrow (ABT.annotation t) i $ relax' nonArrow v o
| Type.ForallsNamed' vs b <- t =
Type.foralls loc vs $ relax' nonArrow v b
Type.foralls loc vs $ relax' nonArrow v b
| Type.Effect' es r <- t,
Type.Arrow' i o <- r =
Type.effect loc es . Type.arrow (ABT.annotation t) i $ relax' nonArrow v o
Type.effect loc es . Type.arrow (ABT.annotation t) i $ relax' nonArrow v o
| Type.Effect' es r <- t =
if any open es then t else Type.effect loc (tv : es) r
if any open es then t else Type.effect loc (tv : es) r
| nonArrow = Type.effect loc [tv] t
| otherwise = t
where
@ -2165,11 +2165,11 @@ check m0 t0 = scope (InCheck m0 t0) $ do
Left m -> failWith $ DuplicateDefinitions m
Right m
| not (wellformedType ctx t0) ->
failWith $ IllFormedType ctx
failWith $ IllFormedType ctx
| Type.Var' TypeVar.Existential {} <- t0 ->
applyM t0 >>= checkWanted [] m
applyM t0 >>= checkWanted [] m
| otherwise ->
checkWanted [] m (Type.stripIntroOuters t0)
checkWanted [] m (Type.stripIntroOuters t0)
-- | `subtype ctx t1 t2` returns successfully if `t1` is a subtype of `t2`.
-- This may have the effect of altering the context.
@ -2184,10 +2184,10 @@ subtype tx ty = scope (InSubtype tx ty) $ do
go _ (Type.Ref' r) (Type.Ref' r2) | r == r2 = pure () -- `Unit`
go ctx t1@(Type.Var' (TypeVar.Universal v1)) t2@(Type.Var' (TypeVar.Universal v2)) -- `Var`
| v1 == v2 && wellformedType ctx t1 && wellformedType ctx t2 =
pure ()
pure ()
go ctx t1@(Type.Var' (TypeVar.Existential _ v1)) t2@(Type.Var' (TypeVar.Existential _ v2)) -- `Exvar`
| v1 == v2 && wellformedType ctx t1 && wellformedType ctx t2 =
pure ()
pure ()
go _ (Type.Arrow' i1 o1) (Type.Arrow' i2 o2) = do
-- `-->`
subtype i2 i1
@ -2226,13 +2226,13 @@ subtype tx ty = scope (InSubtype tx ty) $ do
go ctx (Type.Var' (TypeVar.Existential b v)) t -- `InstantiateL`
| Set.member v (existentials ctx)
&& notMember v (Type.freeVars t) = do
e <- extendExistential Var.inferAbility
instantiateL b v (relax' False e t)
e <- extendExistential Var.inferAbility
instantiateL b v (relax' False e t)
go ctx t (Type.Var' (TypeVar.Existential b v)) -- `InstantiateR`
| Set.member v (existentials ctx)
&& notMember v (Type.freeVars t) = do
e <- extendExistential Var.inferAbility
instantiateR (relax' False e t) b v
e <- extendExistential Var.inferAbility
instantiateR (relax' False e t) b v
go _ (Type.Effects' es1) (Type.Effects' es2) =
subAbilities ((,) Nothing <$> es1) es2
go _ t t2@(Type.Effects' _) | expand t = subtype (Type.effects (loc t) [t]) t2
@ -2255,7 +2255,7 @@ equate t1 t2 = scope (InEquate t1 t2) $ do
where
guardWF ctx t@(Type.Var' _)
| not $ wellformedType ctx t =
failWith (TypeMismatch ctx)
failWith (TypeMismatch ctx)
guardWF _ _ = pure ()
equate0 ::
@ -2269,20 +2269,20 @@ equate0 t1@(Type.Var' tv1) t2@(Type.Var' tv2)
| TypeVar.Universal v1 <- tv1,
TypeVar.Universal v2 <- tv2,
v1 == v2 =
pure ()
pure ()
| TypeVar.Existential b1 v1 <- tv1,
TypeVar.Existential b2 v2 <- tv2 =
if v1 == v2
then pure ()
else do
ctx <- getContext
if ordered ctx v1 v2
then instantiateL b2 v2 t1
else instantiateL b1 v1 t2
if v1 == v2
then pure ()
else do
ctx <- getContext
if ordered ctx v1 v2
then instantiateL b2 v2 t1
else instantiateL b1 v1 t2
| TypeVar.Existential b v1 <- tv1 =
instantiateL b v1 t2
instantiateL b v1 t2
| TypeVar.Existential b v2 <- tv2 =
instantiateL b v2 t1
instantiateL b v2 t1
equate0 (Type.Forall' t01) (Type.Forall' t02) = do
v <- ABT.freshen t02 freshenTypeVar
markThenRetract0 v $ do
@ -2307,12 +2307,12 @@ equate0 (Type.Effect1' e1 a1) (Type.Effect1' e2 a2) = do
equate a1 a2
equate0 (Type.Var' (TypeVar.Existential b v)) t
| notMember v (Type.freeVars t) =
-- subtyping relaxes here, should equality
instantiateL b v t
-- subtyping relaxes here, should equality
instantiateL b v t
equate0 t (Type.Var' (TypeVar.Existential b v))
| notMember v (Type.freeVars t) =
-- subtyping relaxes here, should equality
instantiateL b v t
-- subtyping relaxes here, should equality
instantiateL b v t
equate0 (Type.Effects' es1) (Type.Effects' es2) =
equateAbilities es1 es2
equate0 y1 y2 = do
@ -2340,8 +2340,8 @@ instantiateL blank v (Type.stripIntroOuters -> t) =
go ctx = case t of
Type.Var' (TypeVar.Existential _ v2)
| ordered ctx v v2 -> -- InstLReach (both are existential, set v2 = v)
solve ctx v2 (Type.Monotype (existentialp (loc t) v))
>>= maybe (failWith $ TypeMismatch ctx) setContext
solve ctx v2 (Type.Monotype (existentialp (loc t) v))
>>= maybe (failWith $ TypeMismatch ctx) setContext
Type.Arrow' i o -> do
-- InstLArr
[i', o'] <- traverse freshenVar [nameFrom Var.inferInput i, nameFrom Var.inferOutput o]
@ -2431,18 +2431,18 @@ refineEffectVar _ [] _ _ _ = pure ()
refineEffectVar l es blank v tv
| ev <- TypeVar.Existential blank v,
any (\e -> ev `Set.member` Type.freeVars e) es =
getContext >>= failWith . AbilityCheckFailure [tv] es
getContext >>= failWith . AbilityCheckFailure [tv] es
| otherwise = do
slack <- freshenVar Var.inferAbility
evs <- traverse (\e -> freshenVar (nameFrom Var.inferAbility e)) es
let locs = loc <$> es
es' = zipWith existentialp locs evs
t' = Type.effects l (existentialp l slack : es')
s = Solved blank v (Type.Monotype t')
vs = existential slack : fmap existential evs
replaceContext (existential v) (vs ++ [s])
Foldable.for_ (es `zip` evs) $ \(e, ev) ->
getContext >>= \ctx -> instantiateR (apply ctx e) B.Blank ev
slack <- freshenVar Var.inferAbility
evs <- traverse (\e -> freshenVar (nameFrom Var.inferAbility e)) es
let locs = loc <$> es
es' = zipWith existentialp locs evs
t' = Type.effects l (existentialp l slack : es')
s = Solved blank v (Type.Monotype t')
vs = existential slack : fmap existential evs
replaceContext (existential v) (vs ++ [s])
Foldable.for_ (es `zip` evs) $ \(e, ev) ->
getContext >>= \ctx -> instantiateR (apply ctx e) B.Blank ev
-- | Instantiate the given existential such that it is
-- a supertype of the given type, updating the context
@ -2461,8 +2461,8 @@ instantiateR (Type.stripIntroOuters -> t) blank v =
go ctx = case t of
Type.Var' (TypeVar.Existential _ v2)
| ordered ctx v v2 -> -- InstRReach (both are existential, set v2 = v)
solve ctx v2 (Type.Monotype (existentialp (loc t) v))
>>= maybe (failWith $ TypeMismatch ctx) setContext
solve ctx v2 (Type.Monotype (existentialp (loc t) v))
>>= maybe (failWith $ TypeMismatch ctx) setContext
Type.Arrow' i o -> do
-- InstRArrow
[i', o'] <- traverse freshenVar [nameFrom Var.inferInput i, nameFrom Var.inferOutput o]
@ -2570,15 +2570,15 @@ matchConcrete ::
matchConcrete common acc [] _ = pure (reverse acc, common)
matchConcrete common acc (l : ls) rs
| Just v <- find (headMatch l) common = do
equate v l
ls <- expandAbilities ls
rs <- expandAbilities rs
matchConcrete common acc ls rs
equate v l
ls <- expandAbilities ls
rs <- expandAbilities rs
matchConcrete common acc ls rs
| Just v <- find (headMatch l) rs = do
equate v l
ls <- expandAbilities ls
rs <- expandAbilities rs
matchConcrete (l : common) acc ls rs
equate v l
ls <- expandAbilities ls
rs <- expandAbilities rs
matchConcrete (l : common) acc ls rs
| otherwise = matchConcrete common (l : acc) ls rs
pruneConcrete ::
@ -2592,10 +2592,10 @@ pruneConcrete ::
pruneConcrete _ acc [] _ = pure (reverse acc)
pruneConcrete missing acc ((loc, w) : ws) have
| Just v <- find (headMatch w) have = do
subtype v w `orElse` missing loc w
ws <- expandWanted ws
have <- expandAbilities have
pruneConcrete missing acc ws have
subtype v w `orElse` missing loc w
ws <- expandWanted ws
have <- expandAbilities have
pruneConcrete missing acc ws have
| otherwise = pruneConcrete missing ((loc, w) : acc) ws have
matchVariables ::
@ -2608,7 +2608,7 @@ matchVariables ::
([Type v loc], [Type v loc], [Type v loc])
matchVariables com acc (l : ls) rs
| isExistential l && any (== l) rs =
matchVariables (l : com) acc (filter (/= l) ls) (filter (/= l) rs)
matchVariables (l : com) acc (filter (/= l) ls) (filter (/= l) rs)
| otherwise = matchVariables com (l : acc) ls rs
where
isExistential (Type.Var' TypeVar.Existential {}) = True
@ -2693,11 +2693,11 @@ equateAbilities ls rs =
(vrs, crs) = partition isExistential rs
mlSlack
| [t@(Type.Var' (TypeVar.Existential b v))] <- vls =
Just (loc t, b, v)
Just (loc t, b, v)
| otherwise = Nothing
mrSlack
| [t@(Type.Var' (TypeVar.Existential b v))] <- vrs =
Just (loc t, b, v)
Just (loc t, b, v)
| otherwise = Nothing
in case liftA2 (,) mlSlack mrSlack of
Just ((ll, bl, lSlack), (lr, br, rSlack)) ->
@ -2706,7 +2706,7 @@ equateAbilities ls rs =
| [t@(Type.Var' (TypeVar.Existential bc cv))] <- com,
null vls,
null vrs ->
refine True [(loc t, bc, cv)] [cls ++ crs]
refine True [(loc t, bc, cv)] [cls ++ crs]
| [] <- com, null rs, null cls -> for_ vls defaultAbility
| [] <- com, null ls, null crs -> for_ vrs defaultAbility
| [] <- com, Just pl <- mlSlack, null cls -> refine False [pl] [rs]
@ -2738,7 +2738,8 @@ equateAbilities ls rs =
| u == v = EQ
| ordered ctx u v = LT
| otherwise = GT
cn | common = [Var.inferAbility] | otherwise = []
cn | common = [Var.inferAbility]
| otherwise = []
subAbilities ::
Var v =>
@ -2787,10 +2788,10 @@ subAmbient ::
subAmbient die ambient r
-- find unsolved existential, 'e, that appears in ambient
| (b, e') : _ <- unsolveds = do
-- introduce fresh existential 'e2 to context
e2' <- extendExistential e'
let et2 = Type.effects (loc r) [r, existentialp (loc r) e2']
instantiateR et2 b e' `orElse` die
-- introduce fresh existential 'e2 to context
e2' <- extendExistential e'
let et2 = Type.effects (loc r) [r, existentialp (loc r) e2']
instantiateR et2 b e' `orElse` die
| otherwise = die
where
unsolveds = (ambient >>= Type.flattenEffects >>= vars)
@ -2811,19 +2812,19 @@ abilityCheckSingle die ambient r
-- Ex: given `a`, where there's an exact variable
-- If yes for `a` in ambient, do `subtype a r` and done.
| Just a <- find (headMatch r) ambient =
subtype a r `orElse` die
subtype a r `orElse` die
-- It's an unsolved existential, instantiate it to all of ambient
| Type.Var' tv@(TypeVar.Existential b v) <- r =
let et2 = Type.effects (loc r) ambient
acyclic
| Set.member tv (Type.freeVars et2) =
-- just need to trigger `orElse` in this case
getContext >>= failWith . TypeMismatch
| otherwise = instantiateR et2 b v
in -- instantiate it to `{}` if can't cover all of ambient
acyclic
`orElse` instantiateR (Type.effects (loc r) []) b v
`orElse` die
let et2 = Type.effects (loc r) ambient
acyclic
| Set.member tv (Type.freeVars et2) =
-- just need to trigger `orElse` in this case
getContext >>= failWith . TypeMismatch
| otherwise = instantiateR et2 b v
in -- instantiate it to `{}` if can't cover all of ambient
acyclic
`orElse` instantiateR (Type.effects (loc r) []) b v
`orElse` die
| otherwise = subAmbient die ambient r
headMatch :: Var v => Ord loc => Type v loc -> Type v loc -> Bool

7
parser-typechecker/unison-parser-typechecker.cabal
View File

@ -1,6 +1,6 @@
cabal-version: 1.12
-- This file has been generated from package.yaml by hpack version 0.34.4.
-- This file has been generated from package.yaml by hpack version 0.35.0.
--
-- see: https://github.com/sol/hpack
@ -93,6 +93,7 @@ library
Unison.Parsers
Unison.PrettyPrintEnv
Unison.PrettyPrintEnv.FQN
Unison.PrettyPrintEnv.MonadPretty
Unison.PrettyPrintEnv.Names
Unison.PrettyPrintEnv.Util
Unison.PrettyPrintEnvDecl
@ -298,9 +299,9 @@ library
, x509-system
, yaml
, zlib
default-language: Haskell2010
if flag(optimized)
ghc-options: -funbox-strict-fields -O2
default-language: Haskell2010
test-suite parser-typechecker-tests
type: exitcode-stdio-1.0
@ -486,6 +487,6 @@ test-suite parser-typechecker-tests
, x509-system
, yaml
, zlib
default-language: Haskell2010
if flag(optimized)
ghc-options: -funbox-strict-fields -O2
default-language: Haskell2010

14
unison-cli/src/Unison/CommandLine/DisplayValues.hs
View File

@ -1,5 +1,4 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
module Unison.CommandLine.DisplayValues where
@ -17,6 +16,7 @@ import qualified Unison.ConstructorType as CT
import qualified Unison.DataDeclaration as DD
import Unison.Prelude
import qualified Unison.PrettyPrintEnv as PPE
import Unison.PrettyPrintEnv.MonadPretty (runPretty)
import qualified Unison.PrettyPrintEnv.Util as PPE
import qualified Unison.PrettyPrintEnvDecl as PPE
import Unison.Reference (Reference)
@ -246,10 +246,9 @@ displayPretty pped terms typeOf eval types tm = go tm
typeOf r >>= \case
Nothing -> pure $ termName (PPE.suffixifiedPPE pped) r
Just typ ->
pure . P.group $
TypePrinter.prettySignaturesCTCollapsed
(PPE.suffixifiedPPE pped)
[(r, PPE.termName (PPE.suffixifiedPPE pped) r, typ)]
pure . P.group
. runPretty (PPE.suffixifiedPPE pped)
$ TypePrinter.prettySignaturesCTCollapsed [(r, PPE.termName (PPE.suffixifiedPPE pped) r, typ)]
goColor c = case c of
DD.AnsiColorBlack -> P.black
@ -311,9 +310,8 @@ displayDoc pped terms typeOf evaluated types = go
typeOf r >>= \case
Nothing -> pure $ termName (PPE.unsuffixifiedPPE pped) r
Just typ ->
pure . P.group $
pure . P.group . runPretty (PPE.suffixifiedPPE pped) $
TypePrinter.prettySignaturesCTCollapsed
(PPE.suffixifiedPPE pped)
[(r, PPE.termName (PPE.unsuffixifiedPPE pped) r, typ)]
prettyEval terms r = case r of
Referent.Ref (Reference.Builtin n) -> pure . P.syntaxToColor $ P.text n
@ -329,7 +327,7 @@ displayDoc pped terms typeOf evaluated types = go
let ppe = PPE.declarationPPE pped ref
in terms ref >>= \case
Nothing -> pure $ "😶 Missing term source for: " <> termName ppe r
Just tm -> pure . P.syntaxToColor $ P.group $ TP.prettyBinding ppe (PPE.termName ppe r) tm
Just tm -> pure . P.syntaxToColor . P.group . runPretty ppe $ TP.prettyBinding (PPE.termName ppe r) tm
Referent.Con (ConstructorReference r _) _ -> prettyType r
prettyType r =
let ppe = PPE.declarationPPE pped r

48
unison-cli/src/Unison/CommandLine/OutputMessages.hs
View File

@ -102,6 +102,7 @@ import qualified Unison.NamesWithHistory as Names
import Unison.Parser.Ann (Ann, startingLine)
import Unison.Prelude
import qualified Unison.PrettyPrintEnv as PPE
import Unison.PrettyPrintEnv.MonadPretty (runPretty)
import qualified Unison.PrettyPrintEnv.Util as PPE
import qualified Unison.PrettyPrintEnvDecl as PPED
import Unison.PrettyTerminal
@ -299,21 +300,20 @@ notifyNumbered o = case o of
else
first
( \p ->
( P.lines
[ P.wrap $
"The changes summarized below are available for you to review,"
<> "using the following command:",
"",
P.indentN 2 $
IP.makeExampleNoBackticks
IP.loadPullRequest
[ (prettyReadRemoteNamespace baseRepo),
(prettyReadRemoteNamespace headRepo)
],
"",
p
]
)
P.lines
[ P.wrap $
"The changes summarized below are available for you to review,"
<> "using the following command:",
"",
P.indentN 2 $
IP.makeExampleNoBackticks
IP.loadPullRequest
[ prettyReadRemoteNamespace baseRepo,
prettyReadRemoteNamespace headRepo
],
"",
p
]
)
(showDiffNamespace HideNumbers ppe (absPathToBranchId Path.absoluteEmpty) (absPathToBranchId Path.absoluteEmpty) diff)
-- todo: these numbers aren't going to work,
@ -689,7 +689,7 @@ notifyUser dir o = case o of
TestIncrementalOutputStart ppe (n, total) r _src -> do
putPretty' $
P.shown (total - n) <> " tests left to run, current test: "
<> (P.syntaxToColor $ prettyHashQualified (PPE.termName ppe $ Referent.Ref r))
<> P.syntaxToColor (prettyHashQualified (PPE.termName ppe $ Referent.Ref r))
pure mempty
TestIncrementalOutputEnd _ppe (_n, _total) _r result -> do
clearCurrentLine
@ -1039,7 +1039,7 @@ notifyUser dir o = case o of
P.bracket . P.lines $
P.wrap "The watch expression(s) reference these definitions:" :
"" :
[ (P.syntaxToColor $ TermPrinter.prettyBinding ppe (HQ.unsafeFromVar v) b)
[ P.syntaxToColor . runPretty ppe $ TermPrinter.prettyBinding (HQ.unsafeFromVar v) b
| (v, b) <- bindings
]
prettyWatches =
@ -1815,7 +1815,7 @@ notifyUser dir o = case o of
let referenceText = P.text . Reference.toText . Cv.reference2to1
pure $
P.columnNHeader
["Kind", "Name", "Change", "Ref"]
["Kind", "Name", "Change", "Ref"]
( (termNameAdds <&> \(n, ref) -> ["Term", prettyName n, "Added", referentText ref])
<> (termNameRemovals <&> \(n, ref) -> ["Term", prettyName n, "Removed", referentText ref])
<> (typeNameAdds <&> \(n, ref) -> ["Type", prettyName n, "Added", referenceText ref])
@ -1976,7 +1976,7 @@ displayDefinitions' ppe0 types terms = P.syntaxToColor $ P.sep "\n\n" (prettyTyp
P.hang
("builtin " <> prettyHashQualified n <> " :")
(TypePrinter.prettySyntax (ppeBody r) typ)
UserObject tm -> TermPrinter.prettyBinding (ppeBody r) n tm
UserObject tm -> runPretty (ppeBody r) $ TermPrinter.prettyBinding n tm
go2 ((n, r), dt) =
case dt of
MissingObject r -> missing n r
@ -2081,7 +2081,7 @@ displayDefinitions outputLoc ppe types terms =
P.hang
("builtin " <> prettyHashQualified n <> " :")
(TypePrinter.prettySyntax (ppeBody n r) typ)
UserObject tm -> TermPrinter.prettyBinding (ppeBody n r) n tm
UserObject tm -> runPretty (ppeBody n r) $ TermPrinter.prettyBinding n tm
go2 ((n, r), dt) =
case dt of
MissingObject r -> missing n r
@ -2148,7 +2148,7 @@ unsafePrettyTermResultSig' ::
Pretty
unsafePrettyTermResultSig' ppe = \case
SR'.TermResult' name (Just typ) r _aliases ->
head (TypePrinter.prettySignaturesCT ppe [(r, name, typ)])
head (runPretty ppe $ TypePrinter.prettySignaturesCT [(r, name, typ)])
_ -> error "Don't pass Nothing"
-- produces:
@ -2165,7 +2165,7 @@ unsafePrettyTermResultSigFull' ppe = \case
[ P.hiBlack "-- " <> greyHash (HQ.fromReferent r),
P.group $
P.commas (fmap greyHash $ hq : map HQ'.toHQ (toList aliases)) <> " : "
<> (P.syntaxToColor $ TypePrinter.pretty0 ppe mempty (-1) typ),
<> P.syntaxToColor (TypePrinter.prettySyntax ppe typ),
mempty
]
_ -> error "Don't pass Nothing"
@ -2396,7 +2396,7 @@ todoOutput ppe todo = runNumbered do
termNumbers <- for filteredTerms \(ref, _, _) -> do
n <- addNumberedArg (HQ.toString $ PPE.termName ppeu ref)
pure $ formatNum n
let formattedTerms = TypePrinter.prettySignaturesCT ppes filteredTerms
let formattedTerms = runPretty ppes $ TypePrinter.prettySignaturesCT filteredTerms
numberedTerms = zipWith (<>) termNumbers formattedTerms
pure $
Monoid.unlessM (TO.noEdits todo) . P.callout "🚧" . P.sep "\n\n" . P.nonEmpty $
@ -2407,7 +2407,7 @@ todoOutput ppe todo = runNumbered do
),
P.indentN 2 . P.lines $
( (prettyDeclPair ppeu <$> toList frontierTypes)
++ TypePrinter.prettySignaturesCT ppes (goodTerms frontierTerms)
++ runPretty ppes (TypePrinter.prettySignaturesCT (goodTerms frontierTerms))
),
P.wrap "I recommend working on them in the following order:",
P.lines $ numberedTypes ++ numberedTerms,

57
unison-share-api/src/Unison/Server/Backend.hs
View File

@ -73,6 +73,7 @@ import qualified Unison.NamesWithHistory as NamesWithHistory
import Unison.Parser.Ann (Ann)
import Unison.Prelude
import qualified Unison.PrettyPrintEnv as PPE
import Unison.PrettyPrintEnv.MonadPretty (runPretty)
import qualified Unison.PrettyPrintEnv.Util as PPE
import qualified Unison.PrettyPrintEnvDecl as PPED
import qualified Unison.PrettyPrintEnvDecl.Names as PPED
@ -144,7 +145,7 @@ data BackendError
| MissingSignatureForTerm Reference
| NoSuchDefinition (HQ.HashQualified Name)
data BackendEnv = BackendEnv
newtype BackendEnv = BackendEnv
{ -- | Whether to use the sqlite name-lookup table to generate Names objects rather than building Names from the root branch.
useNamesIndex :: Bool
}
@ -265,7 +266,7 @@ termEntryDisplayName :: TermEntry v a -> Text
termEntryDisplayName = HQ'.toText . termEntryHQName
termEntryHQName :: TermEntry v a -> HQ'.HashQualified NameSegment
termEntryHQName (TermEntry {termEntryName, termEntryConflicted, termEntryHash}) =
termEntryHQName TermEntry {termEntryName, termEntryConflicted, termEntryHash} =
if termEntryConflicted
then HQ'.HashQualified termEntryName termEntryHash
else HQ'.NameOnly termEntryName
@ -283,7 +284,7 @@ typeEntryDisplayName :: TypeEntry -> Text
typeEntryDisplayName = HQ'.toText . typeEntryHQName
typeEntryHQName :: TypeEntry -> HQ'.HashQualified NameSegment
typeEntryHQName (TypeEntry {typeEntryName, typeEntryConflicted, typeEntryReference}) =
typeEntryHQName TypeEntry {typeEntryName, typeEntryConflicted, typeEntryReference} =
if typeEntryConflicted
then HQ'.HashQualified typeEntryName (Reference.toShortHash typeEntryReference)
else HQ'.NameOnly typeEntryName
@ -528,7 +529,7 @@ formatTypeName' ppe r =
termEntryToNamedTerm ::
Var v => PPE.PrettyPrintEnv -> Maybe Width -> TermEntry v a -> NamedTerm
termEntryToNamedTerm ppe typeWidth te@(TermEntry {termEntryType = mayType, termEntryTag = tag, termEntryHash}) =
termEntryToNamedTerm ppe typeWidth te@TermEntry {termEntryType = mayType, termEntryTag = tag, termEntryHash} =
NamedTerm
{ termName = termEntryHQName te,
termHash = termEntryHash,
@ -537,7 +538,7 @@ termEntryToNamedTerm ppe typeWidth te@(TermEntry {termEntryType = mayType, termE
}
typeEntryToNamedType :: TypeEntry -> NamedType
typeEntryToNamedType te@(TypeEntry {typeEntryTag, typeEntryHash}) =
typeEntryToNamedType te@TypeEntry {typeEntryTag, typeEntryHash} =
NamedType
{ typeName = typeEntryHQName $ te,
typeHash = typeEntryHash,
@ -672,7 +673,7 @@ makeTypeSearch :: Int -> NamesWithHistory -> Search Reference
makeTypeSearch len names =
Search
{ lookupNames = \ref -> NamesWithHistory.typeName len ref names,
lookupRelativeHQRefs' = \name -> NamesWithHistory.lookupRelativeHQType' name names,
lookupRelativeHQRefs' = (`NamesWithHistory.lookupRelativeHQType'` names),
matchesNamedRef = HQ'.matchesNamedReference,
makeResult = SR.typeResult
}
@ -682,7 +683,7 @@ makeTermSearch :: Int -> NamesWithHistory -> Search Referent
makeTermSearch len names =
Search
{ lookupNames = \ref -> NamesWithHistory.termName len ref names,
lookupRelativeHQRefs' = \name -> NamesWithHistory.lookupRelativeHQTerm' name names,
lookupRelativeHQRefs' = (`NamesWithHistory.lookupRelativeHQTerm'` names),
matchesNamedRef = HQ'.matchesNamedReferent,
makeResult = SR.termResult
}
@ -721,7 +722,7 @@ hqNameQuery ::
NameSearch ->
[HQ.HashQualified Name] ->
m QueryResult
hqNameQuery codebase (NameSearch {typeSearch, termSearch}) hqs = do
hqNameQuery codebase NameSearch {typeSearch, termSearch} hqs = do
-- Split the query into hash-only and hash-qualified-name queries.
let (hashes, hqnames) = partitionEithers (map HQ'.fromHQ2 hqs)
-- Find the terms with those hashes.
@ -747,8 +748,12 @@ hqNameQuery codebase (NameSearch {typeSearch, termSearch}) hqs = do
-- Now do the actual name query
resultss = map (\name -> applySearch typeSearch name <> applySearch termSearch name) hqnames
(misses, hits) =
zip hqnames resultss
& map (\(hqname, results) -> if null results then Left hqname else Right results)
zipWith
( \hqname results ->
(if null results then Left hqname else Right results)
)
hqnames
resultss
& partitionEithers
-- Handle query misses correctly
missingRefs =
@ -776,7 +781,7 @@ data DefinitionResults v = DefinitionResults
}
expandShortBranchHash ::
Monad m => Codebase m v a -> ShortBranchHash -> Backend m (Branch.CausalHash)
Monad m => Codebase m v a -> ShortBranchHash -> Backend m Branch.CausalHash
expandShortBranchHash codebase hash = do
hashSet <- lift $ Codebase.branchHashesByPrefix codebase hash
len <- lift $ Codebase.branchHashLength codebase
@ -787,18 +792,17 @@ expandShortBranchHash codebase hash = do
throwError . AmbiguousBranchHash hash $ Set.map (SBH.fromHash len) hashSet
-- | Efficiently resolve a root hash and path to a shallow branch's causal.
getShallowCausalAtPathFromRootHash :: Monad m => Codebase m v a -> Maybe (Branch.CausalHash) -> Path -> Backend m (V2Branch.CausalBranch m)
getShallowCausalAtPathFromRootHash :: Monad m => Codebase m v a -> Maybe Branch.CausalHash -> Path -> Backend m (V2Branch.CausalBranch m)
getShallowCausalAtPathFromRootHash codebase mayRootHash path = do
shallowRoot <- case mayRootHash of
Nothing -> lift (Codebase.getShallowRootCausal codebase)
Just h -> do
lift $ Codebase.getShallowCausalForHash codebase (Cv.causalHash1to2 h)
causal <- lift $ Codebase.getShallowCausalAtPath codebase path (Just shallowRoot)
pure causal
lift $ Codebase.getShallowCausalAtPath codebase path (Just shallowRoot)
formatType' :: Var v => PPE.PrettyPrintEnv -> Width -> Type v a -> SyntaxText
formatType' ppe w =
Pretty.render w . TypePrinter.pretty0 ppe mempty (-1)
Pretty.render w . TypePrinter.prettySyntax ppe
formatType :: Var v => PPE.PrettyPrintEnv -> Width -> Type v a -> Syntax.SyntaxText
formatType ppe w = mungeSyntaxText . formatType' ppe w
@ -822,7 +826,7 @@ prettyDefinitionsForHQName ::
-- this path.
Path ->
-- | The root branch to use
Maybe (Branch.CausalHash) ->
Maybe Branch.CausalHash ->
Maybe Width ->
-- | Whether to suffixify bindings in the rendered syntax
Suffixify ->
@ -995,7 +999,7 @@ docsInBranchToHtmlFiles runtime codebase root currentPath directory = do
let currentBranch = Branch.getAt' currentPath root
let allTerms = (R.toList . Branch.deepTerms . Branch.head) currentBranch
-- ignores docs inside lib namespace, recursively
let notLib (_, name) = all (/= "lib") (Name.segments name)
let notLib (_, name) = "lib" `notElem` Name.segments name
docTermsWithNames <- filterM (isDoc codebase . fst) (filter notLib allTerms)
let docNamesByRef = Map.fromList docTermsWithNames
hqLength <- Codebase.hashLength codebase
@ -1069,7 +1073,8 @@ bestNameForTerm ppe width =
Text.pack
. Pretty.render width
. fmap UST.toPlain
. TermPrinter.pretty0 @v ppe TermPrinter.emptyAc
. runPretty ppe
. TermPrinter.pretty0 @v TermPrinter.emptyAc
. Term.fromReferent mempty
bestNameForType ::
@ -1078,7 +1083,7 @@ bestNameForType ppe width =
Text.pack
. Pretty.render width
. fmap UST.toPlain
. TypePrinter.pretty0 @v ppe mempty (-1)
. TypePrinter.prettySyntax @v ppe
. Type.ref ()
-- | Returns (parse, pretty, local, ppe) where:
@ -1096,9 +1101,9 @@ scopedNamesForBranchHash codebase mbh path = do
Nothing
| shouldUseNamesIndex -> indexNames
| otherwise -> do
rootBranch <- lift $ Codebase.getRootBranch codebase
let (parseNames, _prettyNames, localNames) = namesForBranch rootBranch (AllNames path)
pure (parseNames, localNames)
rootBranch <- lift $ Codebase.getRootBranch codebase
let (parseNames, _prettyNames, localNames) = namesForBranch rootBranch (AllNames path)
pure (parseNames, localNames)
Just rootCausal -> do
let ch = V2Causal.causalHash rootCausal
let v1CausalHash = Cv.causalHash2to1 ch
@ -1255,8 +1260,8 @@ termsToSyntax suff width ppe0 terms =
DisplayObject.UserObject tm ->
DisplayObject.UserObject
. Pretty.render width
. TermPrinter.prettyBinding (ppeBody r) n
$ tm
. runPretty (ppeBody r)
$ TermPrinter.prettyBinding n tm
typesToSyntax ::
Var v =>
@ -1296,8 +1301,8 @@ typesToSyntax suff width ppe0 types =
typeToSyntaxHeader ::
Width ->
HQ.HashQualified Name ->
(DisplayObject () (DD.Decl Symbol Ann)) ->
(DisplayObject SyntaxText SyntaxText)
DisplayObject () (DD.Decl Symbol Ann) ->
DisplayObject SyntaxText SyntaxText
typeToSyntaxHeader width hqName obj =
case obj of
BuiltinObject _ ->

16
unison-share-api/src/Unison/Server/Doc.hs
View File

@ -1,6 +1,4 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE OverloadedStrings #-}
@ -32,6 +30,7 @@ import qualified Unison.Codebase.Editor.DisplayObject as DO
import qualified Unison.ConstructorReference as ConstructorReference
import qualified Unison.DataDeclaration as DD
import qualified Unison.PrettyPrintEnv as PPE
import Unison.PrettyPrintEnv.MonadPretty (runPretty)
import qualified Unison.PrettyPrintEnvDecl as PPE
import Unison.Reference (Reference)
import qualified Unison.Reference as Reference
@ -183,16 +182,15 @@ renderDoc pped terms typeOf eval types tm =
formatPrettyType ppe typ = formatPretty (TypePrinter.prettySyntax ppe typ)
source :: Term v () -> m SyntaxText
source tm = (pure . formatPretty . TermPrinter.prettyBlock' True (PPE.suffixifiedPPE pped)) tm
source tm = pure . formatPretty $ TermPrinter.prettyBlock' True (PPE.suffixifiedPPE pped) tm
goSignatures :: [Referent] -> m [P.Pretty SSyntaxText]
goSignatures rs =
runMaybeT (traverse (MaybeT . typeOf) rs) >>= \case
Nothing -> pure ["🆘 codebase is missing type signature for these definitions"]
Just types ->
pure . fmap P.group $
pure . fmap P.group . runPretty (PPE.suffixifiedPPE pped) $
TypePrinter.prettySignaturesST
(PPE.suffixifiedPPE pped)
[(r, PPE.termName (PPE.suffixifiedPPE pped) r, ty) | (r, ty) <- zip rs types]
goSpecial :: Term v () -> m SpecialForm
@ -314,12 +312,12 @@ renderDoc pped terms typeOf eval types tm =
typ <- fromMaybe (Type.builtin () "unknown") <$> typeOf (Referent.Ref ref)
let name = PPE.termName ppe (Referent.Ref ref)
let folded =
formatPretty . P.lines $
TypePrinter.prettySignaturesST ppe [(Referent.Ref ref, name, typ)]
formatPretty . P.lines . runPretty ppe $
TypePrinter.prettySignaturesST [(Referent.Ref ref, name, typ)]
let full tm@(Term.Ann' _ _) _ =
formatPretty (TermPrinter.prettyBinding ppe name tm)
formatPretty (runPretty ppe $ TermPrinter.prettyBinding name tm)
full tm typ =
formatPretty (TermPrinter.prettyBinding ppe name (Term.ann () tm typ))
formatPretty (runPretty ppe $ TermPrinter.prettyBinding name (Term.ann () tm typ))
pure (DO.UserObject (Src folded (full tm typ)))
Term.RequestOrCtor' (view ConstructorReference.reference_ -> r) | Set.notMember r seen -> (: acc) <$> goType r
_ -> pure acc