Skip to content
This repository has been archived by the owner on Oct 18, 2021. It is now read-only.

Commit

Permalink
Add lifted tuples and lists
Browse files Browse the repository at this point in the history
  • Loading branch information
Matheus Magalhães de Alcantara authored and SquidDev committed Oct 29, 2019
1 parent 2e63129 commit 5363e95
Show file tree
Hide file tree
Showing 29 changed files with 101 additions and 79 deletions.
3 changes: 3 additions & 0 deletions src/Core/Lower/Basic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,10 @@ lowerType (S.TyWildcard _) = error "impossible lowerType TyWildcard"
lowerType (S.TyParens t) = lowerType t
lowerType (S.TyWithConstraints _ t) = lowerType t
lowerType S.TyType = StarTy

-- All "lifted" types can just be *, screw Lint
lowerType S.TyLit{} = StarTy
lowerType S.TyTupleL{} = StarTy

-- | Lower a literal from "Syntax" to one from "Core.Core".
lowerLiteral :: Lit -> Literal
Expand Down
18 changes: 17 additions & 1 deletion src/Parser.y
Original file line number Diff line number Diff line change
Expand Up @@ -595,13 +595,17 @@ TypeAtom :: { Located (Type Parsed) }
| type { lPos1 $1 TyType }
| lazy { lPos1 $1 $ TyCon (Name (T.pack "lazy")) }
| '(' ')' { lPos2 $1 $2 $ TyCon (Name (T.pack "unit")) }
| '(' Type ')' { lPos2 $1 $3 $ TyParens (getL $2) }
| '(' List1(Type,',') ')' { lPos2 $1 $3 $ mkTupleTypeL (map getL $2) }
| '[' List1(Type,',') ']' { lPos2 $1 $3 $ mkListTypeL (map getL $2) }
| '(' TypeOperatorF ')' { lPos2 $1 $3 $ TyParens (TyCon $2) }
| '{' ListT(TypeRow, ',') '}' { lPos2 $1 $3 $ TyExactRows $2 }
| '{' Type '|' ListT(TypeRow, ',') '}' { lPos2 $1 $5 $ TyRows (getL $2) $4 }
| '_' { lPos1 $1 (TyWildcard Nothing) }

| string { lPos1 $1 $ TyLit (LiStr (getString $1)) }
| int { lPos1 $1 $ TyLit (LiInt (getInt $1)) }
| true { lPos1 $1 $ TyLit (LiBool True) }
| false { lPos1 $1 $ TyLit (LiBool False) }

TypeRow :: { (T.Text, Type Parsed) }
: ident ':' Type { (getIdent $1, getL $3) }
Expand Down Expand Up @@ -707,6 +711,18 @@ respanFun :: (Spanned a, Spanned b) => a -> b -> Expr Parsed -> Expr Parsed
respanFun s e (Fun p b _) = Fun p b (mkSpanUnsafe (spanStart (annotation s)) (spanEnd (annotation e)))
respanFun _ _ _ = error "what"

mkTupleTypeL :: [Type p] -> Type p
mkTupleTypeL [x] = TyParens x
mkTupleTypeL (x:xs) =
let go [x] = x
go (x:xs) = TyTupleL x (go xs)
go [] = undefined
in go (x:xs)

mkListTypeL :: [Type Parsed] -> Type Parsed
mkListTypeL [] = TyPromotedCon (Name (T.pack "Nil"))
mkListTypeL (x:xs) = TyApp (TyPromotedCon (Name (T.pack "Cons"))) (TyTupleL x (mkListTypeL xs))

buildClass :: TopAccess -> Located (Type Parsed) -> [Fundep Parsed]
-> [ClassItem Parsed] -> Parser (Span -> Toplevel Parsed)
buildClass am (L parsed typ) fundep ms =
Expand Down
1 change: 1 addition & 0 deletions src/Syntax/Desugar.hs
Original file line number Diff line number Diff line change
Expand Up @@ -171,6 +171,7 @@ ty (TyPi b p) = TyPi (binder b) (ty p)
ty (TyRows t fs) = TyRows (ty t) (map (second ty) fs)
ty (TyExactRows fs) = TyExactRows (map (second ty) fs)
ty (TyTuple l r) = TyTuple (ty l) (ty r)
ty (TyTupleL l r) = TyTupleL (ty l) (ty r)
ty (TyWildcard t) = TyWildcard (ty <$> t)
ty TySkol{} = error "TySkol in desugar"
ty TyWithConstraints{} = error "TywithConstraints in desugar"
Expand Down
4 changes: 4 additions & 0 deletions src/Syntax/Implicits.hs
Original file line number Diff line number Diff line change
Expand Up @@ -258,6 +258,7 @@ getHead t@TyLit{} = (t, Seq.empty)
getHead t@TyWildcard{} = (t, Seq.empty)
getHead (TyParens t) = getHead t
getHead t@TyOperator{} = (t, Seq.empty)
getHead t@TyTupleL{} = (t, Seq.empty)

-- | Split the type of an implicit variable into its head and a set of
-- obligations.
Expand Down Expand Up @@ -334,6 +335,9 @@ matches (TyTuple a b) (TyApp f x) =

matches TyTuple{} _ = False

matches (TyTupleL a b) (TyTupleL a' b') = a `matches` a' && b `matches` b'
matches (TyTupleL _ _) _ = False

matches (TySkol v) (TySkol v') = v == v'
matches TySkol{} _ = False

Expand Down
4 changes: 4 additions & 0 deletions src/Syntax/Pretty.hs
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ applyCons (TyApp a b) = TyApp (applyCons a) (applyCons b)
applyCons (TyRows r rs) = TyRows (applyCons r) (map (second applyCons) rs)
applyCons (TyExactRows rs) = TyExactRows (map (second applyCons) rs)
applyCons (TyTuple a b) = TyTuple (applyCons a) (applyCons b)
applyCons (TyTupleL a b) = TyTupleL (applyCons a) (applyCons b)
applyCons (TyParens t) = TyParens (applyCons t)
applyCons (TyOperator l o r) = TyOperator (applyCons l) o (applyCons r)
applyCons (TyWithConstraints cs a) =
Expand Down Expand Up @@ -61,6 +62,7 @@ displayType = prettyType . dropKindVars mempty where
dropKindVars s (TyRows t rs) = TyRows (dropKindVars s t) (map (second (dropKindVars s)) rs)
dropKindVars s (TyExactRows rs) = TyExactRows (map (second (dropKindVars s)) rs)
dropKindVars m (TyTuple s t) = TyTuple (dropKindVars m s) (dropKindVars m t)
dropKindVars m (TyTupleL s t) = TyTupleL (dropKindVars m s) (dropKindVars m t)
dropKindVars s (TyWithConstraints cs t) = TyWithConstraints cs (dropKindVars s t)
dropKindVars s (TyParens t) = TyParens (dropKindVars s t)
dropKindVars s (TyOperator l o r) = TyOperator (dropKindVars s l) o (dropKindVars s r)
Expand All @@ -82,6 +84,7 @@ displayType = prettyType . dropKindVars mempty where
kindVarIn v (TyApp t y) = kindVarIn v t && kindVarIn v y
kindVarIn v (TyRows t rs) = kindVarIn v t && all (kindVarIn v . snd) rs
kindVarIn v (TyExactRows rs) = all (kindVarIn v . snd) rs
kindVarIn v (TyTupleL t y) = kindVarIn v t && kindVarIn v y
kindVarIn v (TyTuple t y) = kindVarIn v t && kindVarIn v y
kindVarIn v (TyWithConstraints _ t) = kindVarIn v t
kindVarIn v (TyParens t) = kindVarIn v t
Expand Down Expand Up @@ -140,6 +143,7 @@ prettyType (TyApp x e) = parenTyFun x (displayType x) <+> parenTyArg e (displayT
prettyType (TyRows p rows) = enclose (lbrace <> space) (space <> rbrace) $
pretty p <+> soperator pipe <+> hsep (punctuate comma (displayRows rows))
prettyType (TyExactRows rows) = record (displayRows rows)
prettyType (TyTupleL x y) = parens $ prettyType x <> comma <+> prettyType y
prettyType (TyTuple t s) =
parenTyFun t (displayType t) <+> soperator (char '*') <+> parenTuple s (displayType s)
prettyType t@TyWithConstraints{} = displayType (applyCons t)
Expand Down
1 change: 1 addition & 0 deletions src/Syntax/Raise.hs
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ raiseT v (TySkol (Skolem n u t m)) = TySkol (Skolem (v n) (v u) (raiseT v t) (mo
raiseT v (TyVar n) = TyVar (v n)
raiseT v (TyApp x y) = TyApp (raiseT v x) (raiseT v y)
raiseT v (TyTuple x y) = TyTuple (raiseT v x) (raiseT v y)
raiseT v (TyTupleL x y) = TyTupleL (raiseT v x) (raiseT v y)
raiseT v (TyRows rho rows) = TyRows (raiseT v rho) (map (second (raiseT v)) rows)
raiseT v (TyExactRows rows) = TyExactRows (map (second (raiseT v)) rows)
raiseT v (TyWithConstraints eq a) = TyWithConstraints (map (bimap (raiseT v) (raiseT v)) eq) (raiseT v a)
Expand Down
1 change: 1 addition & 0 deletions src/Syntax/Resolve.hs
Original file line number Diff line number Diff line change
Expand Up @@ -447,6 +447,7 @@ reType r (TyRows t f) = TyRows <$> reType r t
<*> traverse (\(a, b) -> (a,) <$> reType r b) f
reType r (TyExactRows f) = TyExactRows <$> traverse (\(a, b) -> (a,) <$> reType r b) f
reType r (TyTuple ta tb) = TyTuple <$> reType r ta <*> reType r tb
reType r (TyTupleL ta tb) = TyTupleL <$> reType r ta <*> reType r tb
reType _ (TyWildcard _) = pure (TyWildcard Nothing)
reType r (TyParens t) = TyParens <$> reType r t
reType r (TyOperator tl o tr) = TyOperator <$> reType r tl <*> (lookupTy o `catchJunk` r) <*> reType r tr
Expand Down
4 changes: 4 additions & 0 deletions src/Syntax/Subst.hs
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ instance Ord (Var p) => Substitutable p (Type p) where
ftv (TyWildcard v) = foldMap ftv v
ftv (TyApp a b) = ftv a <> ftv b
ftv (TyTuple a b) = ftv a <> ftv b
ftv (TyTupleL a b) = ftv a <> ftv b
ftv (TyRows rho rows) = ftv rho <> foldMap (ftv . snd) rows
ftv (TyExactRows rows) = foldMap (ftv . snd) rows
ftv (TyWithConstraints eq b) = foldMap (\(a, b) -> ftv a <> ftv b) eq <> ftv b
Expand All @@ -58,6 +59,7 @@ instance Ord (Var p) => Substitutable p (Type p) where
apply s t@(TyVar v) = Map.findWithDefault t v s
apply s (TyApp a b) = TyApp (apply s a) (apply s b)
apply s (TyTuple a b) = TyTuple (apply s a) (apply s b)
apply s (TyTupleL a b) = TyTupleL (apply s a) (apply s b)
apply s (TyPi binder t) = TyPi (apply s binder) (apply s' t) where
s' = foldr Map.delete s (Set.toList (bound binder))
apply s (TyRows rho rows) = TyRows (apply s rho) (map (second (apply s)) rows)
Expand Down Expand Up @@ -166,6 +168,7 @@ tyVarOcc TyWildcard{} = mempty
tyVarOcc (TyVar v) = singletonOcc v
tyVarOcc (TyApp a b) = tyVarOcc a <> tyVarOcc b
tyVarOcc (TyTuple a b) = tyVarOcc a <> tyVarOcc b
tyVarOcc (TyTupleL a b) = tyVarOcc a <> tyVarOcc b
tyVarOcc (TyRows rho rows) = tyVarOcc rho <> foldMap (tyVarOcc . snd) rows
tyVarOcc (TyExactRows rows) = foldMap (tyVarOcc . snd) rows
tyVarOcc (TyParens t) = tyVarOcc t
Expand All @@ -189,6 +192,7 @@ nominalTvs (TyVar v) = Set.singleton v
nominalTvs (TyWildcard _) = mempty
nominalTvs (TyApp a b) = nominalTvs a <> nominalTvs b
nominalTvs (TyTuple a b) = nominalTvs a <> nominalTvs b
nominalTvs (TyTupleL a b) = nominalTvs a <> nominalTvs b
nominalTvs (TyRows rho rows) = nominalTvs rho <> foldMap (nominalTvs . snd) rows
nominalTvs (TyExactRows rows) = foldMap (nominalTvs . snd) rows
nominalTvs (TyParens t) = nominalTvs t
Expand Down
1 change: 1 addition & 0 deletions src/Syntax/Transform.hs
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ transformType ft = goT where
transT (TyRows f fs) = TyRows (goT f) (map (second goT) fs)
transT (TyExactRows fs) = TyExactRows (map (second goT) fs)
transT (TyTuple l r) = TyTuple (goT l) (goT r)
transT (TyTupleL l r) = TyTupleL (goT l) (goT r)
transT (TyOperator l o r) = TyOperator (goT l) o (goT r)
transT (TyParens t) = TyParens (goT t)

Expand Down
2 changes: 2 additions & 0 deletions src/Syntax/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ data Type p

| TyType -- yeah, type : type, fight me
| TyLit Lit
| TyTupleL (Type p) (Type p) -- A lifted tuple

data TyBinder p
= Anon { _tyBinderType :: Type p } -- ^ A function type
Expand Down Expand Up @@ -213,6 +214,7 @@ instance (Pretty (Var p)) => Pretty (Type p) where
pretty (TyOperator l o r) = pretty l <+> pretty o <+> pretty r

pretty (TyParens t) = parens $ pretty t
pretty (TyTupleL a b) = parens $ pretty a <+> comma <+> pretty b

pretty (TyWithConstraints a b) =
parens (hsep (punctuate comma (map prettyEq a))) <+> soperator (char '') <+> pretty b
Expand Down
1 change: 1 addition & 0 deletions src/Syntax/Verify/Pattern.hs
Original file line number Diff line number Diff line change
Expand Up @@ -473,6 +473,7 @@ inhabited env (AbsState st cs i)
go c (TyWithConstraints _ t) = go c t
go _ TyType = inhb
go _ TyLit{} = inhb
go _ TyTupleL{} = inhb

-- | Returns the type name if this type is concrete (defined as has 0 or more
-- constructors, rather than being abstract).
Expand Down
4 changes: 4 additions & 0 deletions src/Types/Infer/Builtin.hs
Original file line number Diff line number Diff line change
Expand Up @@ -193,6 +193,7 @@ checkWildcard e (TyPi b x) = flip (*>) (checkWildcard e x) $
checkWildcard e (TyRows t rs) = checkWildcard e t *> traverse_ (checkWildcard e . snd) rs
checkWildcard e (TyExactRows rs) = traverse_ (checkWildcard e . snd) rs
checkWildcard e (TyTuple a b) = checkWildcard e a *> checkWildcard e b
checkWildcard e (TyTupleL a b) = checkWildcard e a *> checkWildcard e b
checkWildcard e (TyOperator l _ r) = checkWildcard e l *> checkWildcard e r
checkWildcard e (TyParens t) = checkWildcard e t

Expand Down Expand Up @@ -220,6 +221,7 @@ getHead t@TyWithConstraints{} = t
getHead t@TyType = t
getHead t@TyWildcard{} = t
getHead t@TyOperator{} = t
getHead t@TyTupleL{} = t
getHead (TyParens t) = getHead t

expandTypeWith :: TySyms -> Type Typed -> Type Typed
Expand Down Expand Up @@ -247,6 +249,8 @@ expandTypeWith _ x@TySkol{} = x
expandTypeWith _ x@TyLit{} = x

expandTypeWith s (TyTuple a b) = TyTuple (expandTypeWith s a) (expandTypeWith s b)
expandTypeWith s (TyTupleL a b) = TyTupleL (expandTypeWith s a) (expandTypeWith s b)

expandTypeWith s (TyPi b r) = TyPi b' (expandTypeWith s r) where
b' = case b of
Anon t -> Anon (expandTypeWith s t)
Expand Down
1 change: 1 addition & 0 deletions src/Types/Infer/Class.hs
Original file line number Diff line number Diff line change
Expand Up @@ -815,6 +815,7 @@ validContext w a t@TySkol{} = dictates (InvalidContext w a t)
validContext w a t@TyWithConstraints{} = dictates (InvalidContext w a t)
validContext w a t@TyType{} = dictates (InvalidContext w a t)
validContext w a t@TyLit{} = dictates (InvalidContext w a t)
validContext w a t@TyTupleL{} = dictates (InvalidContext w a t)
validContext w a (TyParens t) = validContext w a t

tooConcrete :: MonadInfer Typed m => Type Typed -> m Bool
Expand Down
1 change: 1 addition & 0 deletions src/Types/Infer/Function.hs
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,7 @@ recursiveCall :: Var Typed -> Type Typed -> [[Type Typed]]
recursiveCall c (TyApps (TyCon c') args)
| c == c' = [args] | otherwise = concatMap (recursiveCall c) args
recursiveCall c (TyTuple a b) = recursiveCall c a <|> recursiveCall c b
recursiveCall c (TyTupleL a b) = recursiveCall c a <|> recursiveCall c b
recursiveCall c (TyPi b r) =
recursiveCall c r <|> case b of
Anon t -> recursiveCall c t
Expand Down
1 change: 1 addition & 0 deletions src/Types/Infer/Let.hs
Original file line number Diff line number Diff line change
Expand Up @@ -425,6 +425,7 @@ deSkol = go mempty where
go acc (TyWithConstraints cs x) = TyWithConstraints (map (bimap (go acc) (go acc)) cs) (go acc x)
go acc (TyOperator l o r) = TyOperator (go acc l) o (go acc r)
go acc (TyParens p) = TyParens $ go acc p
go acc (TyTupleL a b) = TyTupleL (go acc a) (go acc b)
go _ TyType = TyType

expandTyBindings :: MonadReader Env m => Binding Typed -> m (Binding Typed)
Expand Down
13 changes: 8 additions & 5 deletions src/Types/Kinds.hs
Original file line number Diff line number Diff line change
Expand Up @@ -396,6 +396,11 @@ inferKind (TyApp f x) = do
Invisible{} -> error "inferKind TyApp: visible argument to implicit quantifier"
Implicit{} -> error "inferKind TyApp: visible argument to implicit quantifier"

inferKind (TyTupleL a b) = do
(a, k_a) <- inferKind a
(b, k_b) <- inferKind b
pure (TyTupleL a b, TyTuple k_a k_b)

inferKind (TyRows p rs) = do
(p, k) <- secondA isType =<< inferKind p
rs <- for rs $ \(row, ty) -> do
Expand Down Expand Up @@ -426,9 +431,6 @@ checkKind (TyExactRows rs) k = do
pure (row, ty)
pure (TyExactRows rs)

checkKind (TyTuple a b) (TyTuple ak bk) =
TyTuple <$> checkKind a ak <*> checkKind b bk

checkKind (TyTuple a b) ek =
TyTuple <$> checkKind a ek <*> checkKind b ek

Expand Down Expand Up @@ -557,8 +559,8 @@ closeOver' vars r a = do
promoteOrError :: Type Typed -> Maybe Doc
promoteOrError TyWithConstraints{} = Just (string "mentions constraints")
promoteOrError TyTuple{} = Nothing
promoteOrError TyRows{} = Just (string "mentions a tuple")
promoteOrError TyExactRows{} = Just (string "mentions a tuple")
promoteOrError TyRows{} = Just (string "mentions a record")
promoteOrError TyExactRows{} = Just (string "mentions a record")
promoteOrError (TyApp a b) = promoteOrError a <|> promoteOrError b
promoteOrError (TyPi (Invisible _ a _) b) = join (traverse promoteOrError a) <|> promoteOrError b
promoteOrError (TyPi (Anon a) b) = promoteOrError a <|> promoteOrError b
Expand All @@ -570,6 +572,7 @@ promoteOrError TyPromotedCon{} = Nothing
promoteOrError TyType{} = Nothing
promoteOrError TyWildcard{} = Nothing
promoteOrError TyLit{} = Nothing
promoteOrError TyTupleL{} = Nothing
promoteOrError (TyParens p) = promoteOrError p
promoteOrError (TyOperator l _ r) = promoteOrError l <|> promoteOrError r

Expand Down
6 changes: 2 additions & 4 deletions src/Types/Unify.hs
Original file line number Diff line number Diff line change
Expand Up @@ -287,11 +287,9 @@ doSolve (ohno@(ConImplicit reason scope var cons) :<| cs) = do -- {{{

_ ->
case head (appsView cons) of
TyCon v | Just solve <- magicClass v -> do
TyCon v | Just (solve, report) <- magicClass v -> do
(w, cs) <- censor (const mempty) $ listen $ solve reason scope' old
doSolve (Seq.fromList cs)
`catchChronicle`
\e -> confesses (ArisingFrom (UnsatClassCon reason (apply sub ohno) (MagicErrors (toList e))) reason)
doSolve (Seq.fromList cs) `catchChronicle` report reason old
case w of
Just solution -> solveCoSubst . at var ?= solution
Nothing -> do
Expand Down
5 changes: 5 additions & 0 deletions src/Types/Unify/Equality.hs
Original file line number Diff line number Diff line change
Expand Up @@ -266,6 +266,10 @@ unify scope x@(TyApp f g) y@(TyOperator l v r) =
unify scope (TyOperator l v r) (TyOperator l' v' r')
| v == v' = AppCo <$> unify scope l l' <*> unify scope r r'

unify scope (TyTupleL a b) (TyTupleL a' b') =
(\_ _ -> AssumedCo (TyTupleL a b) (TyTupleL b b'))
<$> unify scope a a' <*> unify scope b b'

unify scope ta@(TyApps (TyCon v) xs@(_:_)) b = do
x <- view solveInfo

Expand Down Expand Up @@ -560,6 +564,7 @@ flatten assum i = runWriterT . go 0 where
go_b (Invisible v k r) = Invisible v <$> traverse (go (l + 1)) k <*> pure r

go l (TyTuple a b) = TyTuple <$> go (l + 1) a <*> go (l + 1) b
go l (TyTupleL a b) = TyTupleL <$> go (l + 1) a <*> go (l + 1) b
go l (TyRows t rs) = TyRows <$> go (l + 1) t <*> traverse (_2 %%~ go (l + 1)) rs
go l (TyExactRows rs) = TyExactRows <$> traverse (_2 %%~ go (l + 1)) rs
go x (TyOperator l o r) = TyOperator <$> go (x + 1) l <*> pure o <*> go (x + 1) r
Expand Down
23 changes: 17 additions & 6 deletions src/Types/Unify/Magic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,9 @@ module Types.Unify.Magic (magicClass, magicTyFun) where
import Control.Monad.Infer
import Control.Lens

import qualified Data.Sequence as Seq
import Data.Foldable

import Syntax.Implicits
import Syntax.Builtin
import Syntax.Pretty
Expand All @@ -19,16 +22,24 @@ import Types.Unify.Base

type Solver m = SomeReason -> ImplicitScope ClassInfo Typed -> Type Typed -> m (Maybe (Wrapper Typed))
type TfSolver m = ImplicitScope ClassInfo Typed -> [Type Typed] -> Type Typed -> m (Maybe (Coercion Typed))
type Reporter m = SomeReason -> Type Typed -> Seq.Seq TypeError -> m ()

magicClass :: MonadSolve m => Var Typed -> Maybe (Solver m)
magicClass :: MonadSolve m => Var Typed -> Maybe (Solver m, Reporter m)
magicClass v
| v == tyKStrName = Just (solveKnownLit knownStrName knownStrTy knownStrTy' tyKStr tyString)
| v == tyKIntName = Just (solveKnownLit knownIntName knownIntTy knownIntTy' tyKInt tyInt)
| v == rowConsName = Just solveRowCons
| v == tyEqName = Just solveEq
| v == tyTypeError_n = Just (\_ _ (TyApps _ [a]) -> solveTypeError a)
| v == tyKStrName = Just (solveKnownLit knownStrName knownStrTy knownStrTy' tyKStr tyString, confess')
| v == tyKIntName = Just (solveKnownLit knownIntName knownIntTy knownIntTy' tyKInt tyInt, confess')
| v == rowConsName = Just (solveRowCons, confess')
| v == tyEqName = Just (solveEq, confess_eq)
| v == tyTypeError_n = Just (\_ _ (TyApps _ [a]) -> solveTypeError a, confess')
| otherwise = Nothing

confess' :: MonadSolve m => Reporter m
confess' reason ts xs = confesses (UnsatClassCon reason (ConImplicit reason mempty undefined ts) (MagicErrors (toList xs)))

confess_eq :: MonadSolve m => Reporter m
confess_eq reason (TyApps _ [a, b]) _ = confesses (ArisingFrom (NotEqual a b) reason)
confess_eq _ _ _ = undefined

solveEq :: MonadSolve m => Solver m
solveEq blame classes ty@(TyApps _ [a, b]) = do
var <- genName
Expand Down
2 changes: 2 additions & 0 deletions src/Types/Wellformed.hs
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ wellformed tp = case tp of
wellformed b
TyApp a b -> wellformed a *> wellformed b
TyTuple a b -> wellformed a *> wellformed b
TyTupleL a b -> wellformed a *> wellformed b
TyRows rho rows -> do
case rho of
TyRows{} -> pure ()
Expand Down Expand Up @@ -56,6 +57,7 @@ skols (TyPi b t)
skols (TyRows r rs) = skols r <> foldMap (skols . snd) rs
skols (TyExactRows rs) = foldMap (skols . snd) rs
skols (TyTuple a b) = skols a <> skols b
skols (TyTupleL a b) = skols a <> skols b
skols (TyWithConstraints cs a) =
foldMap (\(x, y) -> skols x <> skols y) cs <> skols a
skols (TyParens t) = skols t
Expand Down
2 changes: 1 addition & 1 deletion tests/parser/fail_span.out
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
fail_span.ml[1:12 ..1:16]: error
Unexpected match, expected one of forall, '_', type, lazy, '(', '{', identifier, constructor, type variable, int, string
Unexpected match, expected one of forall, '_', true, false, type, lazy, '(', '{', '[', identifier, constructor, type variable, int, string
1 │ let main : match = 1
│ ^^^^^
2 changes: 1 addition & 1 deletion tests/types/class/row-cons-fail.out
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
row-cons-fail.ml[1:9 ..1:39]: error
No instance for row_cons 'record "y" 'type { x : int } arising in the expression
No instance for row_cons 'record "y" 'type { x : int } arising in this expression
1 │ let x = Amc.restrict_row @"y" { x = 1 }
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Expand Down
Loading

0 comments on commit 5363e95

Please sign in to comment.