diff --git a/src/Core/Lower/Basic.hs b/src/Core/Lower/Basic.hs
index 0b7343c74..0b5e11d08 100644
--- a/src/Core/Lower/Basic.hs
+++ b/src/Core/Lower/Basic.hs
@@ -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
diff --git a/src/Parser.y b/src/Parser.y
index c817d9851..30724a4ef 100644
--- a/src/Parser.y
+++ b/src/Parser.y
@@ -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) }
@@ -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 =
diff --git a/src/Syntax/Desugar.hs b/src/Syntax/Desugar.hs
index c0c807b19..ee590fbbd 100644
--- a/src/Syntax/Desugar.hs
+++ b/src/Syntax/Desugar.hs
@@ -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"
diff --git a/src/Syntax/Implicits.hs b/src/Syntax/Implicits.hs
index b8b69f700..3fb881d4f 100644
--- a/src/Syntax/Implicits.hs
+++ b/src/Syntax/Implicits.hs
@@ -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.
@@ -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
 
diff --git a/src/Syntax/Pretty.hs b/src/Syntax/Pretty.hs
index 265877a23..7d2e546a1 100644
--- a/src/Syntax/Pretty.hs
+++ b/src/Syntax/Pretty.hs
@@ -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) =
@@ -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)
@@ -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
@@ -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)
diff --git a/src/Syntax/Raise.hs b/src/Syntax/Raise.hs
index 979cc91ec..b0053ad55 100644
--- a/src/Syntax/Raise.hs
+++ b/src/Syntax/Raise.hs
@@ -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)
diff --git a/src/Syntax/Resolve.hs b/src/Syntax/Resolve.hs
index 598be915e..7d72fbf9c 100644
--- a/src/Syntax/Resolve.hs
+++ b/src/Syntax/Resolve.hs
@@ -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
diff --git a/src/Syntax/Subst.hs b/src/Syntax/Subst.hs
index cbc8bfcc0..922dc82e9 100644
--- a/src/Syntax/Subst.hs
+++ b/src/Syntax/Subst.hs
@@ -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
@@ -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)
@@ -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
@@ -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
diff --git a/src/Syntax/Transform.hs b/src/Syntax/Transform.hs
index 59c5d96a2..3f4257ebd 100644
--- a/src/Syntax/Transform.hs
+++ b/src/Syntax/Transform.hs
@@ -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)
 
diff --git a/src/Syntax/Type.hs b/src/Syntax/Type.hs
index f7c88b5fd..1be8e4c82 100644
--- a/src/Syntax/Type.hs
+++ b/src/Syntax/Type.hs
@@ -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
@@ -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
diff --git a/src/Syntax/Verify/Pattern.hs b/src/Syntax/Verify/Pattern.hs
index fd6fe42d8..39b6159d8 100644
--- a/src/Syntax/Verify/Pattern.hs
+++ b/src/Syntax/Verify/Pattern.hs
@@ -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).
diff --git a/src/Types/Infer/Builtin.hs b/src/Types/Infer/Builtin.hs
index a14588d2b..52e341dd0 100644
--- a/src/Types/Infer/Builtin.hs
+++ b/src/Types/Infer/Builtin.hs
@@ -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
 
@@ -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
@@ -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)
diff --git a/src/Types/Infer/Class.hs b/src/Types/Infer/Class.hs
index e81da66de..9a6026fb6 100644
--- a/src/Types/Infer/Class.hs
+++ b/src/Types/Infer/Class.hs
@@ -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
diff --git a/src/Types/Infer/Function.hs b/src/Types/Infer/Function.hs
index 21269bbe8..048f0f018 100644
--- a/src/Types/Infer/Function.hs
+++ b/src/Types/Infer/Function.hs
@@ -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
diff --git a/src/Types/Infer/Let.hs b/src/Types/Infer/Let.hs
index 4edc4e344..3f012236c 100644
--- a/src/Types/Infer/Let.hs
+++ b/src/Types/Infer/Let.hs
@@ -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)
diff --git a/src/Types/Kinds.hs b/src/Types/Kinds.hs
index 2f0ddec16..ef1841d44 100644
--- a/src/Types/Kinds.hs
+++ b/src/Types/Kinds.hs
@@ -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
@@ -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
 
@@ -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
@@ -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
 
diff --git a/src/Types/Unify.hs b/src/Types/Unify.hs
index 7ed171bf9..ffd61976c 100644
--- a/src/Types/Unify.hs
+++ b/src/Types/Unify.hs
@@ -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
diff --git a/src/Types/Unify/Equality.hs b/src/Types/Unify/Equality.hs
index 3cf2f4c0b..ec2b8933a 100644
--- a/src/Types/Unify/Equality.hs
+++ b/src/Types/Unify/Equality.hs
@@ -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
 
@@ -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
diff --git a/src/Types/Unify/Magic.hs b/src/Types/Unify/Magic.hs
index cf37612dd..2b29fa112 100644
--- a/src/Types/Unify/Magic.hs
+++ b/src/Types/Unify/Magic.hs
@@ -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
@@ -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
diff --git a/src/Types/Wellformed.hs b/src/Types/Wellformed.hs
index 647cf271a..ded9df8ae 100644
--- a/src/Types/Wellformed.hs
+++ b/src/Types/Wellformed.hs
@@ -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 ()
@@ -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
diff --git a/tests/parser/fail_span.out b/tests/parser/fail_span.out
index 6c2cd60d9..61419ca7d 100644
--- a/tests/parser/fail_span.out
+++ b/tests/parser/fail_span.out
@@ -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
   │            ^^^^^
diff --git a/tests/types/class/row-cons-fail.out b/tests/types/class/row-cons-fail.out
index fdc0681e1..3a3739982 100644
--- a/tests/types/class/row-cons-fail.out
+++ b/tests/types/class/row-cons-fail.out
@@ -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 }
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/tests/types/gadt/fail_term.out b/tests/types/gadt/fail_term.out
index ea6c3e901..fe55182b8 100644
--- a/tests/types/gadt/fail_term.out
+++ b/tests/types/gadt/fail_term.out
@@ -1,18 +1,6 @@
 fail_term.ml[16:3 ..16:30]: error
-  No instance for 'a -> 'b -> 'b ~ 'x -> 'y -> 'x arising in the expression
    │ 
 16 │   Lam (Lam (Var (There Here)))
    │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-  • Because:
-  Could not match the rigid type variable 'b with the type 'a
-
-  • Arising in the expression
-   │ 
-16 │   Lam (Lam (Var (There Here)))
-   │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-  • When checking that this expression
-   │ 
-16 │   Lam (Lam (Var (There Here)))
-   │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-  has type forall 'a 'b. term unit ('a -> 'b -> 'b)
+  Couldn't match actual type 'a -> 'b -> 'b
+    with the type expected by the context, 'x -> 'y -> 'x
diff --git a/tests/types/gadt/fin.out b/tests/types/gadt/fin.out
index 854f75226..6386b2303 100644
--- a/tests/types/gadt/fin.out
+++ b/tests/types/gadt/fin.out
@@ -1,11 +1,6 @@
 fin.ml[11:14 ..11:18]: error
-  No instance for 'n ~ S (S 'k) arising in the expression
    │ 
 11 │   | SS SZ -> FS FZ
    │              ^^^^^
-  • Because:
-   │ 
-11 │   | SS SZ -> FS FZ
-   │              ^^^^^
-  Couldn't match actual type 'n ~ 'n
-    with the type expected by the context, 'n ~ S (S 'k)
+  Couldn't match actual type 'n
+    with the type expected by the context, S (S 'k)
diff --git a/tests/types/gadt/gadt03-fail.out b/tests/types/gadt/gadt03-fail.out
index 96081ff94..241ca249d 100644
--- a/tests/types/gadt/gadt03-fail.out
+++ b/tests/types/gadt/gadt03-fail.out
@@ -1,11 +1,6 @@
 gadt03-fail.ml[8:12 ..8:19]: error
-  No instance for bool ~ int arising in the expression
   │ 
 8 │ let show = function
   │            ^^^^^^^^
-  • Because:
-  │ 
-8 │ let show = function
-  │            ^^^^^^^^
-  Couldn't match actual type bool ~ bool
-    with the type expected by the context, bool ~ int
+  Couldn't match actual type bool
+    with the type expected by the context, int
diff --git a/tests/types/gadt/gadt07-escape-fail.out b/tests/types/gadt/gadt07-escape-fail.out
index cabca8b3b..f8da57ba5 100644
--- a/tests/types/gadt/gadt07-escape-fail.out
+++ b/tests/types/gadt/gadt07-escape-fail.out
@@ -1,16 +1,6 @@
 gadt07-escape-fail.ml[10:3 ..10:17]: error
-  No instance for 'a ~ int arising in the expression
-   │ 
-10 │   match hval with
-   │   ^^^^^^^^^^^^^^^
-  • Because:
-  Could not match the rigid type variable 'a with the type int
-
-  Where the type variable a is an existential,
-  bound by the constructor MkHid, which has type
-     forall 'a. exp 'a * exp 'a -> hidden
-
-  • Arising in the the expression
    │ 
 10 │   match hval with
    │   ^^^^^^^^^^^^^^^
+  Couldn't match actual type 'a
+    with the type expected by the context, int
diff --git a/tests/types/gadt/gadt08-pass.ml b/tests/types/gadt/gadt08-pass.ml
index f47e471ad..2ee3a6b5f 100644
--- a/tests/types/gadt/gadt08-pass.ml
+++ b/tests/types/gadt/gadt08-pass.ml
@@ -3,12 +3,12 @@ type list 'a =
   | Cons : 'a * list 'a -> list 'a
 
 type elem 'x 'xs =
-  | Here : elem 'x (Cons ('x * 'xs))
-  | There : elem 'x 'xs -> elem 'x (Cons ('y * 'xs))
+  | Here : elem 'x (Cons ('x, 'xs))
+  | There : elem 'x 'xs -> elem 'x (Cons ('y, 'xs))
 
 type product 'a =
   | Unit : product Nil
-  | Pair : 'a * product 'b -> product (Cons ('a * 'b))
+  | Pair : 'a * product 'b -> product (Cons ('a, 'b))
 
 let a :: b = Pair (a, b)
 
diff --git a/tests/types/gadt/gadt08-pass.out b/tests/types/gadt/gadt08-pass.out
index a00498197..e17583f88 100644
--- a/tests/types/gadt/gadt08-pass.out
+++ b/tests/types/gadt/gadt08-pass.out
@@ -2,10 +2,10 @@ list : type -> type
 Nil : Spec{'a : type}. list 'a
 Cons : Spec{'a : type}. ('a * list 'a) -> list 'a
 elem : Infer{'a : type}. 'a -> list 'a -> type
-Here : Infer{'fv : type}. Infer{'a : type}. Spec{'xs : 'fv}. Spec{'x : 'a}. Infer{'xs : list 'a}. ('xs ~ Cons ('x * 'xs)) ⊃ elem 'x 'xs
-There : Infer{'hq : type}. Infer{'a : type}. Spec{'xs : 'hq}. Spec{'x : 'a}. Spec{'xs : list 'a}. Infer{'y : 'a}. ('xs ~ Cons ('y * 'xs)) ⊃ elem 'x 'xs -> elem 'x 'xs
+Here : Infer{'ga : type}. Infer{'a : type}. Spec{'xs : 'ga}. Spec{'x : 'a}. Infer{'xs : list 'a}. ('xs ~ Cons ('x , 'xs)) ⊃ elem 'x 'xs
+There : Infer{'hx : type}. Infer{'a : type}. Spec{'xs : 'hx}. Spec{'x : 'a}. Spec{'xs : list 'a}. Infer{'y : 'a}. ('xs ~ Cons ('y , 'xs)) ⊃ elem 'x 'xs -> elem 'x 'xs
 product : list type -> type
-Unit : Infer{'kn : type}. Spec{'a : 'kn}. ('a ~ Nil) ⊃ product 'a
-Pair : Infer{'lu : type}. Spec{'a : 'lu}. Spec{'a : type}. Spec{'b : list type}. ('a ~ Cons ('a * 'b)) ⊃ ('a * product 'b) -> product 'a
-:: : Infer{'a : type}. Infer{'b : list type}. 'a -> product 'b -> product (Cons ('a * 'b))
-foo : product (Cons (int * Cons (unit * Cons (string * Cons (bool * Cons (float * Nil))))))
+Unit : Infer{'kx : type}. Spec{'a : 'kx}. ('a ~ Nil) ⊃ product 'a
+Pair : Infer{'mf : type}. Spec{'a : 'mf}. Spec{'a : type}. Spec{'b : list type}. ('a ~ Cons ('a , 'b)) ⊃ ('a * product 'b) -> product 'a
+:: : Infer{'a : type}. Infer{'b : list type}. 'a -> product 'b -> product (Cons ('a , 'b))
+foo : product (Cons (int , Cons (unit , Cons (string , Cons (bool , Cons (float , Nil))))))
diff --git a/tests/types/nasty_cycle.out b/tests/types/nasty_cycle.out
index e374d3f29..7b0e9cdeb 100644
--- a/tests/types/nasty_cycle.out
+++ b/tests/types/nasty_cycle.out
@@ -10,18 +10,8 @@ nasty_cycle.ml[19:25 ..19:25]: error
 19 │       | Right p -> Left p
    │                         ^
 nasty_cycle.ml[18:26 ..18:32]: error
-  No instance for S 'n ~ S (S 's) arising in the expression
-   │ 
-18 │       | Left p -> Right (Even2 p)
-   │                          ^^^^^^^
-  • Because:
-  Could not match the rigid type variable 's with the type S 's
-
-  Where the type variable s is an existential,
-  bound by the constructor SS, which has type
-     forall 'n 's. snat 's -> snat (S 's)
-
-  • Arising in the the expression
    │ 
 18 │       | Left p -> Right (Even2 p)
    │                          ^^^^^^^
+  Couldn't match actual type S 'n
+    with the type expected by the context, S (S 's)