Report ambiguous type/kind uvars, don't crash

4 files changed, 151 insertions, 124 deletions

diff --git a/src/HSVIS/Diagnostic.hs b/src/HSVIS/Diagnostic.hs
index 116e4cd..2794461 100644
--- a/src/HSVIS/Diagnostic.hs
+++ b/src/HSVIS/Diagnostic.hs
@@ -16,7 +16,7 @@ instance Pretty Pos where
 
 -- | Inclusive-exclusive range of positions in a file.
 data Range = Range Pos Pos
-  deriving (Show)
+  deriving (Show, Eq, Ord)
 
 instance Semigroup Range where
   Range a b <> Range c d = Range (min a c) (max b d)
diff --git a/src/HSVIS/Pretty.hs b/src/HSVIS/Pretty.hs
index cc8cb2a..c25fe08 100644
--- a/src/HSVIS/Pretty.hs
+++ b/src/HSVIS/Pretty.hs
@@ -9,6 +9,10 @@ class Pretty a where
 instance Pretty Void where
   prettysPrec _ = absurd
 
+instance (Pretty a, Pretty b) => Pretty (a, b) where
+  prettysPrec _ (x, y) =
+    showString "(" . prettysPrec 0 x . showString ", " . prettysPrec 1 y . showString ")"
+
 prettyPrec :: Pretty a => Int -> a -> String
 prettyPrec d x = prettysPrec d x ""
 
diff --git a/src/HSVIS/Typecheck.hs b/src/HSVIS/Typecheck.hs
index 8b642eb..2f68232 100644
--- a/src/HSVIS/Typecheck.hs
+++ b/src/HSVIS/Typecheck.hs
@@ -19,7 +19,7 @@ module HSVIS.Typecheck (
 import Control.Monad
 import Data.Bifunctor (first, second, bimap)
 import Data.Foldable (toList)
-import Data.List (inits)
+import Data.List (inits, foldl1')
 import Data.Map.Strict (Map)
 import Data.Maybe (fromMaybe)
 import qualified Data.Map.Strict as Map
@@ -42,13 +42,13 @@ import HSVIS.Typecheck.Solve
 
 data StageTC
 
-type instance X DataDef StageTC = CKind
+type instance X DataDef StageTC = (Range, CKind)
 type instance X DataField StageTC = Range
 type instance X FunDef  StageTC = Range
 type instance X TypeSig StageTC = Maybe Range
 type instance X FunEq   StageTC = ()
 type instance X Kind    StageTC = ()
-type instance X Type    StageTC = CKind
+type instance X Type    StageTC = (Range, CKind)
 type instance X Pattern StageTC = (Range, CType)
 type instance X RHS     StageTC = CType
 type instance X Expr    StageTC = (Range, CType)
@@ -230,8 +230,8 @@ scopeVEnv m = do
 genKUniVar :: TCM CKind
 genKUniVar = KExt () . KUniVar <$> genId
 
-genUniVar :: CKind -> TCM CType
-genUniVar k = TExt k . TUniVar <$> genId
+genUniVar :: Range -> CKind -> TCM CType
+genUniVar rng k = TExt (rng, k) . TUniVar <$> genId
 
 getKind' :: Range -> Name -> TCM CKind
 getKind' rng name = getKind name >>= \case
@@ -246,7 +246,7 @@ getType' :: Range -> Name -> TCM CType
 getType' rng name = getType name >>= \case
   Nothing -> do
     raise SError rng $ "Variable not in scope: " ++ pretty name
-    t <- genUniVar (KType ())  -- insert it now so that all occurrences of this out-of-scope name get the same type
+    t <- genUniVar rng (KType ())  -- insert it now so that all occurrences of this out-of-scope name get the same type
     modifyVEnv (Map.insert name t)
     return t
   Just k -> return k
@@ -292,7 +292,7 @@ prepareDataDef (DataDef _ name params _) = do
 -- Assumes that the kind of the name itself has already been registered with
 -- the correct arity (this is done by prepareDataDef).
 kcDataDef :: (CKind, [CKind]) -> PDataDef -> TCM CDataDef
-kcDataDef (kd, parkinds) (DataDef _ name params cons) = do
+kcDataDef (kd, parkinds) (DataDef defrng name params cons) = do
   -- ensure unicity of type param names
   params' <-
     let prenames = Set.fromList (map snd params)
@@ -311,19 +311,23 @@ kcDataDef (kd, parkinds) (DataDef _ name params cons) = do
         DataField (extOf t) <$> kcType KCTMNormal (Just (KType ())) t
       return (cname, fields')
 
-  return (DataDef kd name (zip parkinds params') cons')
+  let params_ranges = map fst params
+  return (DataDef (defrng, kd) name (zip (zip params_ranges parkinds) params') cons')
 
 generateInvCons :: CDataDef -> [(Name, InvCon)]
-generateInvCons (DataDef k tname params cons) =
-  let tyvars = Map.fromList (map swap params)
-      resty = TApp (KType ()) (TCon k tname) (map (uncurry TVar) params)
+generateInvCons (DataDef (defrng, k) tname params cons) =
+  let tyvars = Map.fromList [(n, k1) | ((_rng, k1), n) <- params]
+      -- defrng is a bit imprecise here, but it's fine
+      resty = TApp (defrng, KType ()) (TCon (defrng, k) tname) (map (uncurry TVar) params)
   in [(cname, InvCon tyvars resty (map dataFieldType fields)) | (cname, fields) <- cons]
 
 generateConstructors :: CDataDef -> [(Name, CType)]
-generateConstructors (DataDef k tname params cons) =
-  let resty = TApp (KType ()) (TCon k tname) (map (uncurry TVar) params)
-  in [let funty = foldr (TFun (KType ())) resty (map dataFieldType fields)
-      in (cname, foldr (\(k1, n1) -> TExt (KType ()) . TForallC (n1, k1)) funty params)
+generateConstructors (DataDef (defrng, k) tname params cons) =
+  -- using defrng is again a bit imprecise here
+  let resty = TApp (defrng, KType ()) (TCon (defrng, k) tname) (map (uncurry TVar) params)
+  in [let funty = foldr (TFun (defrng, KType ())) resty (map dataFieldType fields)
+      in (cname, foldr (\((_, k1), n1) -> TExt (defrng, KType ()) . TForallC (n1, k1))
+                       funty params)
      | (cname, fields) <- cons]
 
 promoteDownK :: Maybe CKind -> TCM CKind
@@ -357,43 +361,45 @@ kcType' mode mdown = \case
     (ext1, t') <- kcType' mode Nothing t
     (ext2, ts') <- sequence <$> mapM (kcType' mode Nothing) ts  -- TODO: give more useful down kinds
     retk <- promoteDownK mdown
-    let expected = foldr (KFun ()) retk (map extOf ts')
-    emit $ CEqK (extOf t') expected rng
-    return (ext1 <> ext2, TApp retk t' ts')
+    let expected = foldr (KFun ()) retk (map (snd . extOf) ts')
+    emit $ CEqK (snd (extOf t')) expected rng
+    return (ext1 <> ext2, TApp (rng, retk) t' ts')
 
   TTup rng ts -> do
     (ext, ts') <- sequence <$> mapM (kcType' mode (Just (KType ()))) ts
     downEqK rng mdown (KType ())
-    return (ext, TTup (KType ()) ts')
+    return (ext, TTup (rng, KType ()) ts')
 
   TList rng t -> do
     (ext, t') <- kcType' mode (Just (KType ())) t
     downEqK rng mdown (KType ())
-    return (ext, TList (KType ()) t')
+    return (ext, TList (rng, KType ()) t')
 
   TFun rng t1 t2 -> do
     (ext1, t1') <- kcType' mode (Just (KType ())) t1
     (ext2, t2') <- kcType' mode (Just (KType ())) t2
     downEqK rng mdown (KType ())
-    return (ext1 <> ext2, TFun (KType ()) t1' t2')
+    return (ext1 <> ext2, TFun (rng, KType ()) t1' t2')
 
   TCon rng n -> do
     k <- getKind' rng n
     downEqK rng mdown k
-    return (mempty, TCon k n)
+    return (mempty, TCon (rng, k) n)
 
   TVar rng n -> do
     mk <- getKind n
     case mk of
       Nothing -> do
         k <- promoteDownK mdown
-        return (case mode of KCTMNormal -> ()
-                             KCTMOpen -> MMap.singleton n (pure k)
-               ,TVar k n)
+        case mode of
+          KCTMNormal -> do
+            raise SError rng $ "Type variable out of scope: " ++ pretty n
+            return ((), TVar (rng, k) n)
+          KCTMOpen -> return (MMap.singleton n (pure k), TVar (rng, k) n)
       Just k -> do
         downEqK rng mdown k
         -- TODO: need to instantiate top-level foralls in k here
-        return (mempty, TVar k n)
+        return (mempty, TVar (rng, k) n)
 
   TExt rng (TForallP n mk1 t) -> do  -- implicit forall
     k1 <- maybe genKUniVar (return . checkKind) mk1
@@ -402,12 +408,13 @@ kcType' mode mdown = \case
     (ext, t') <- scopeTEnv $ do
       modifyTEnv (Map.insert n k1)
       kcType' mode (Just k2) t
-    return (ext, TExt k2 (TForallC (n, k1) t'))  -- 'k2', not 'k1 -> k2', because the forall is implicit
+    return (ext, TExt (rng, k2) (TForallC (n, k1) t'))  -- 'k2', not 'k1 -> k2', because the forall is implicit
 
 tcFunDefBlock :: [PFunDef] -> TCM [CFunDef]
 tcFunDefBlock fdefs = do
+  let funrange = foldl1' (<>) (map extOf fdefs)
   -- collect types for each of the bound functions, or unification variables if there's no type signature
-  bound <- mapM (\(FunDef _ n ts _) -> (n,) <$> tcTypeSig ts) fdefs
+  bound <- mapM (\(FunDef _ n ts _) -> (n,) <$> tcTypeSig funrange ts) fdefs
   defs' <- scopeVEnv $ do
     modifyVEnv (Map.fromList [(n, t) | (n, TypeSig _ t) <- bound] <>)
     forM (zip fdefs bound) $ \(def, (_, sig)) ->
@@ -426,11 +433,15 @@ checkKind :: PKind -> CKind
 checkKind (KType ()) = KType ()
 checkKind (KFun () k1 k2) = KFun () (checkKind k1) (checkKind k2)
 
-tcTypeSig :: PTypeSig -> TCM CTypeSig
-tcTypeSig (TypeSig () sig) = do
+-- | The 'Range' argument is the range of the entire function; used in case there
+-- is no type signature.
+tcTypeSig :: Range -> PTypeSig -> TCM CTypeSig
+tcTypeSig _ (TypeSig () sig) = do
   (typ, freetvars) <- kcType KCTMOpen (Just (KType ())) sig
-  return $ TypeSig (Just (extOf sig)) $ foldr (\(n, k) -> TExt (KType ()) . TForallC (n, k)) typ (Map.assocs freetvars)
-tcTypeSig (TypeSigExt () NoTypeSig) = TypeSig Nothing <$> genUniVar (KType ())
+  return $ TypeSig (Just (extOf sig)) $
+             foldr (\(n, k) -> TExt (extOf sig, KType ()) . TForallC (n, k))
+                   typ (Map.assocs freetvars)
+tcTypeSig funrange (TypeSigExt () NoTypeSig) = TypeSig Nothing <$> genUniVar funrange (KType ())
 
 -- | Typechecks the function definition, but assumes its signature has already
 -- been checked, and is passed separately. Thus the PTypeSig in the PFunDef is
@@ -468,7 +479,7 @@ tcPattern down = \case
   PCon rng n ps ->
     getInvCon n >>= \case
       Just (InvCon tyvars match fields) -> do
-        unisub <- mapM genUniVar tyvars  -- substitution for the universally quantified variables
+        unisub <- mapM (genUniVar rng) tyvars  -- substitution for the universally quantified variables
         let match' = substType mempty mempty unisub match
             fields' = map (substType mempty mempty unisub) fields
         emit $ CEq down match' rng
@@ -480,8 +491,8 @@ tcPattern down = \case
   POp rng p1 op p2 ->
     case op of
       OCons -> do
-        eltty <- genUniVar (KType ())
-        let listty = TList (KType ()) eltty
+        eltty <- genUniVar rng (KType ())
+        let listty = TList (rng, KType ()) eltty
         emit $ CEq down listty rng
         p1' <- tcPattern eltty p1
         p2' <- tcPattern listty p2
@@ -491,15 +502,16 @@ tcPattern down = \case
         return (PWildcard (rng, down))
 
   PList rng ps -> do
-    eltty <- genUniVar (KType ())
-    let listty = TList (KType ()) eltty
+    eltty <- genUniVar rng (KType ())
+    let listty = TList (rng, KType ()) eltty
     emit $ CEq down listty rng
     PList (rng, listty) <$> mapM (tcPattern eltty) ps
 
   PTup rng ps -> do
-    ts <- mapM (\_ -> genUniVar (KType ())) ps
-    emit $ CEq down (TTup (KType ()) ts) rng
-    PTup (rng, TTup (KType ()) ts) <$> zipWithM tcPattern ts ps
+    ts <- mapM (\p -> genUniVar (extOf p) (KType ())) ps
+    let typ = TTup (rng, KType ()) ts
+    emit $ CEq down typ rng
+    PTup (rng, typ) <$> zipWithM tcPattern ts ps
 
 tcRHS :: CType -> PRHS -> TCM CRHS
 tcRHS _ (Guarded _ _) = error "typecheck: Guards not yet supported"
@@ -511,58 +523,61 @@ tcExpr :: CType -> PExpr -> TCM CExpr
 tcExpr down = \case
   ELit rng lit -> do
     let ty = case lit of
-               LInt{} -> TCon (KType ()) (Name "Int")
-               LFloat{} -> TCon (KType ()) (Name "Double")
-               LChar{} -> TCon (KType ()) (Name "Char")
-               LString{} -> TList (KType ()) (TCon (KType ()) (Name "Char"))
+               LInt{} -> TCon (rng, KType ()) (Name "Int")
+               LFloat{} -> TCon (rng, KType ()) (Name "Double")
+               LChar{} -> TCon (rng, KType ()) (Name "Char")
+               LString{} -> TList (rng, KType ()) (TCon (rng, KType ()) (Name "Char"))
     emit $ CEq down ty rng
     return $ ELit (rng, ty) lit
 
   EVar rng n -> do
     ty <- getType' rng n
-    ty' <- instantiateTForallsUni ty
+    ty' <- instantiateTForallsUni rng ty
     emit $ CEq down ty' rng
     return $ EVar (rng, ty') n
 
   ECon rng n -> do
     ty <- getType' rng n
-    ty' <- instantiateTForallsUni ty
+    ty' <- instantiateTForallsUni rng ty
     emit $ CEq down ty' rng
     return $ EVar (rng, ty') n
 
   EList rng es -> do
-    eltty <- genUniVar (KType ())
-    let listty = TList (KType ()) eltty
+    eltty <- genUniVar rng (KType ())
+    let listty = TList (rng, KType ()) eltty
     emit $ CEq down listty rng
     EList (rng, listty) <$> mapM (tcExpr listty) es
 
   ETup rng es -> do
-    ts <- mapM (\_ -> genUniVar (KType ())) es
-    emit $ CEq down (TTup (KType ()) ts) rng
-    ETup (rng, TTup (KType ()) ts) <$> zipWithM tcExpr ts es
+    ts <- mapM (\_ -> genUniVar rng (KType ())) es
+    let typ = TTup (rng, KType ()) ts
+    emit $ CEq down typ rng
+    ETup (rng, typ) <$> zipWithM tcExpr ts es
 
   EApp rng e1 es -> do
-    argtys <- mapM (\_ -> genUniVar (KType ())) es
-    let funty = foldr (TFun (KType ())) down argtys
+    argtys <- mapM (\e -> genUniVar (extOf e) (KType ())) es
+    let funty = foldr (TFun (rng, KType ())) down argtys
     EApp (rng, funty) <$> tcExpr funty e1
                       <*> zipWithM tcExpr argtys es
 
   -- TODO: these types are way too monomorphic and in any case these
   -- ~operators~ functions should not be built-in
   EOp rng e1 op e2 -> do
-    let int = TCon (KType ()) (Name "Int")
-        bool = TCon (KType ()) (Name "Bool")
+    let int = \r -> TCon (r, KType ()) (Name "Int")
+        bool = \r -> TCon (r, KType ()) (Name "Bool")
+        rng1 = extOf e1
+        rng2 = extOf e2
     (rty, aty1, aty2) <- case op of
-      OAdd -> return (int, int, int)
-      OSub -> return (int, int, int)
-      OMul -> return (int, int, int)
-      ODiv -> return (int, int, int)
-      OMod -> return (int, int, int)
-      OEqu -> return (bool, int, int)
-      OPow -> return (int, int, int)
+      OAdd -> return (int rng, int rng1, int rng2)
+      OSub -> return (int rng, int rng1, int rng2)
+      OMul -> return (int rng, int rng1, int rng2)
+      ODiv -> return (int rng, int rng1, int rng2)
+      OMod -> return (int rng, int rng1, int rng2)
+      OEqu -> return (bool rng, int rng1, int rng2)
+      OPow -> return (int rng, int rng1, int rng2)
       OCons -> do
-        eltty <- genUniVar (KType ())
-        let listty = TList (KType ()) eltty
+        eltty <- genUniVar rng1 (KType ())
+        let listty = TList (rng2, KType ()) eltty
         return (listty, eltty, listty)
     emit $ CEq down rty rng
     e1' <- tcExpr aty1 e1
@@ -570,13 +585,13 @@ tcExpr down = \case
     return (EOp (rng, rty) e1' op e2')
 
   EIf rng e1 e2 e3 -> do
-    e1' <- tcExpr (TCon (KType ()) (Name "Bool")) e1
+    e1' <- tcExpr (TCon (rng, KType ()) (Name "Bool")) e1
     e2' <- tcExpr down e2
     e3' <- tcExpr down e3
     return (EIf (rng, down) e1' e2' e3')
 
   ECase rng e1 alts -> do
-    ty <- genUniVar (KType ())
+    ty <- genUniVar rng (KType ())
     e1' <- tcExpr ty e1
     alts' <- forM alts $ \(pat, rhs) ->
       scopeVEnv $
@@ -593,11 +608,12 @@ tcExpr down = \case
 
   EError rng -> return $ EError (rng, down)
 
-instantiateTForallsUni :: CType -> TCM CType
-instantiateTForallsUni = go mempty
+-- | The 'Range' is the place where the type is being instantiated.
+instantiateTForallsUni :: Range -> CType -> TCM CType
+instantiateTForallsUni instRng = go mempty
   where
     go sub (TExt _ (TForallC (n, k1) t)) = do
-      var <- genUniVar k1
+      var <- genUniVar instRng k1
       go (Map.insert n var sub) t
     go sub t = return $ substType mempty mempty sub t
 
@@ -607,9 +623,9 @@ unfoldFunTy rng n (TFun _ t1 t2) = do
   (params, core) <- unfoldFunTy rng (n - 1) t2
   return (t1 : params, core)
 unfoldFunTy rng n t = do
-  vars <- replicateM n (genUniVar (KType ()))
-  core <- genUniVar (KType ())
-  let expected = foldr (TFun (KType ())) core vars
+  vars <- replicateM n (genUniVar rng (KType ()))
+  core <- genUniVar rng (KType ())
+  let expected = foldr (TFun (rng, KType ())) core vars
   emit $ CEq expected t rng
   return (vars, core)
 
@@ -708,8 +724,8 @@ solveTypeVars cs = do
       (TCon _ n1, TCon _ n2) | n1 == n2 -> mempty
       (TVar _ n1, TVar _ n2) | n1 == n2 -> mempty
       -- TODO: this doesn't check that the types are kind-correct. Did we already check that?
-      (TExt _ (TForallC (n1, k) t1), TExt _ (TForallC (n2, _) t2)) ->
-        reduce t1 (substType mempty mempty (Map.singleton n2 (TVar k n1)) t2) rng
+      (TExt (rng1, _) (TForallC (n1, k) t1), TExt _ (TForallC (n2, _) t2)) ->
+        reduce t1 (substType mempty mempty (Map.singleton n2 (TVar (rng1, k) n1)) t2) rng
 
       -- otherwise, this is a kind mismatch
       (k1, k2) -> (mempty, pure (k1, k2, rng))
@@ -738,9 +754,9 @@ substProg :: Map Int CKind -> Map Int CType -> CProgram -> CProgram
 substProg mk mt (Program ds fs) = Program (map (substDdef mk mt) ds) (map (substFdef mk mt) fs)
 
 substDdef :: Map Int CKind -> Map Int CType -> CDataDef -> CDataDef
-substDdef mk mt (DataDef k name pars cons) =
-  DataDef (substKind mk k) name
-          (map (first (substKind mk)) pars)
+substDdef mk mt (DataDef (defrng, k) name pars cons) =
+  DataDef (defrng, substKind mk k) name
+          (map (first (second (substKind mk))) pars)
           (map (second (map (substDataField mk mt))) cons)
 
 substDataField :: Map Int CKind -> Map Int CType -> CDataField -> CDataField
@@ -795,14 +811,14 @@ substExpr mk mt = go
 substType :: Map Int CKind -> Map Int CType -> Map Name CType -> CType -> CType
 substType mk mt mtv = go
   where
-    go (TApp k t ts) = TApp (goKind k) (go t) (map go ts)
-    go (TTup k ts) = TTup (goKind k) (map go ts)
-    go (TList k t) = TList (goKind k) (go t)
-    go (TFun k t1 t2) = TFun (goKind k) (go t1) (go t2)
-    go (TCon k n) = TCon (goKind k) n
-    go (TVar k n) = fromMaybe (TVar (goKind k) n) (Map.lookup n mtv)
-    go (TExt k (TUniVar v)) = fromMaybe (TExt (goKind k) (TUniVar v)) (Map.lookup v mt)
-    go (TExt k (TForallC (n, k1) t)) = TExt (goKind k) (TForallC (n, goKind k1) (go t))
+    go (TApp (rng, k) t ts) = TApp (rng, goKind k) (go t) (map go ts)
+    go (TTup (rng, k) ts) = TTup (rng, goKind k) (map go ts)
+    go (TList (rng, k) t) = TList (rng, goKind k) (go t)
+    go (TFun (rng, k) t1 t2) = TFun (rng, goKind k) (go t1) (go t2)
+    go (TCon (rng, k) n) = TCon (rng, goKind k) n
+    go (TVar (rng, k) n) = fromMaybe (TVar (rng, goKind k) n) (Map.lookup n mtv)
+    go (TExt (rng, k) (TUniVar v)) = fromMaybe (TExt (rng, goKind k) (TUniVar v)) (Map.lookup v mt)
+    go (TExt (rng, k) (TForallC (n, k1) t)) = TExt (rng, goKind k) (TForallC (n, goKind k1) (go t))
 
     goKind = substKind mk
 
@@ -820,18 +836,18 @@ finaliseProg (Program ds fs) =
   Program <$> traverse finaliseDdef ds <*> traverse finaliseFdef fs
 
 finaliseDdef :: MonadRaise m => CDataDef -> m TDataDef
-finaliseDdef (DataDef k name pars cons) =
-  DataDef <$> finaliseKind k <*> pure name
-          <*> traverse (firstM finaliseKind) pars
+finaliseDdef (DataDef (rng, k) name pars cons) =
+  DataDef <$> finaliseKind rng k <*> pure name
+          <*> traverse (firstM (finaliseKind rng . snd)) pars
           <*> traverse (secondM (traverse finaliseDataField)) cons
 
 finaliseDataField :: MonadRaise m => CDataField -> m TDataField
-finaliseDataField (DataField rng t) = DataField rng <$> finaliseType rng t
+finaliseDataField (DataField rng t) = DataField rng <$> finaliseType t
 
 finaliseFdef :: MonadRaise m => CFunDef -> m TFunDef
-finaliseFdef (FunDef rng n (TypeSig msigrng sig) eqs) =
+finaliseFdef (FunDef _ n (TypeSig _ sig) eqs) =
   FunDef () n
-         <$> (TypeSig () <$> finaliseType (fromMaybe rng msigrng) sig)
+         <$> (TypeSig () <$> finaliseType sig)
          <*> traverse finaliseFunEq eqs
 
 finaliseFunEq :: MonadRaise m => CFunEq -> m TFunEq
@@ -842,7 +858,7 @@ finaliseFunEq (FunEq () n ps rhs) =
 
 finaliseRHS :: MonadRaise m => CRHS -> m TRHS
 finaliseRHS (Guarded _ _) = error "typecheck: guards unsupported"
-finaliseRHS (Plain t e) = Plain <$> finaliseType (fst (extOf e)) t <*> finaliseExpr e
+finaliseRHS (Plain t e) = Plain <$> finaliseType t <*> finaliseExpr e
 
 finalisePattern :: MonadRaise m => CPattern -> m TPattern
 finalisePattern = \case
@@ -854,7 +870,7 @@ finalisePattern = \case
   PList e ps -> PList <$> goExt e <*> traverse finalisePattern ps
   PTup e ps -> PTup <$> goExt e <*> traverse finalisePattern ps
   where
-    goExt (rng, t) = finaliseType rng t
+    goExt (_, t) = finaliseType t
 
 finaliseExpr :: MonadRaise m => CExpr -> m TExpr
 finaliseExpr = \case
@@ -870,28 +886,35 @@ finaliseExpr = \case
   ELet e defs body -> ELet <$> goExt e <*> traverse finaliseFdef defs <*> finaliseExpr body
   EError e -> EError <$> goExt e
   where
-    goExt (rng, t) = finaliseType rng t
+    goExt (_, t) = finaliseType t
 
-finaliseType :: MonadRaise m => Range -> CType -> m TType
-finaliseType rng toptype = go toptype
+finaliseType :: MonadRaise m => CType -> m TType
+finaliseType toptype = go toptype
   where
-    go :: MonadRaise m => Type StageTC -> m TType
-    go (TApp k t ts) = TApp <$> finaliseKind k <*> go t <*> traverse go ts
-    go (TTup k ts) = TTup <$> finaliseKind k <*> traverse go ts
-    go (TList k t) = TList <$> finaliseKind k <*> go t
-    go (TFun k t1 t2) = TFun <$> finaliseKind k <*> go t1 <*> go t2
-    go (TCon k n) = TCon <$> finaliseKind k <*> pure n
-    go (TVar k n) = TVar <$> finaliseKind k <*> pure n
-    go t@(TExt k TUniVar{}) = do
+    go :: MonadRaise m => CType -> m TType
+    go (TApp e t ts) = TApp <$> goExt e <*> go t <*> traverse go ts
+    go (TTup e ts) = TTup <$> goExt e <*> traverse go ts
+    go (TList e t) = TList <$> goExt e <*> go t
+    go (TFun e t1 t2) = TFun <$> goExt e <*> go t1 <*> go t2
+    go (TCon e n) = TCon <$> goExt e <*> pure n
+    go (TVar e n) = TVar <$> goExt e <*> pure n
+    go t@(TExt (rng, k) TUniVar{}) = do
       raise SError rng $ "Ambiguous type unification variable " ++ pretty t ++ " in type: " ++ pretty toptype
-      TVar <$> finaliseKind k <*> pure (Name "$_error")
-    go (TExt k (TForallC (n, k1) t)) = TExt <$> finaliseKind k <*> (TForall <$> ((,) <$> pure n <*> finaliseKind k1) <*> go t)
-
-finaliseKind :: MonadRaise m => CKind -> m TKind
-finaliseKind = \case
-  KType () -> pure (KType ())
-  KFun () k1 k2 -> KFun () <$> finaliseKind k1 <*> finaliseKind k2
-  k@(KExt () KUniVar{}) -> error $ "Unresolved kind variable: " ++ pretty k
+      TVar <$> finaliseKind rng k <*> pure (Name "$_error")
+    go (TExt e@(rng, _) (TForallC (n, k1) t)) =
+      TExt <$> goExt e <*> (TForall <$> ((n,) <$> finaliseKind rng k1) <*> go t)
+
+    goExt (rng, t) = finaliseKind rng t
+
+finaliseKind :: MonadRaise m => Range -> CKind -> m TKind
+finaliseKind toprng topkind = go topkind
+  where
+    go :: MonadRaise m => CKind -> m TKind
+    go (KType ()) = pure (KType ())
+    go (KFun () k1 k2) = KFun () <$> go k1 <*> go k2
+    go k@(KExt () KUniVar{}) = do
+      raise SError toprng $ "Ambiguous kind unification variable " ++ pretty k ++ " in kind: " ++ pretty topkind
+      pure $ KType ()
 
 -------------------- END OF FINALISATION FUNCTIONS --------------------
 
diff --git a/src/HSVIS/Typecheck/Solve.hs b/src/HSVIS/Typecheck/Solve.hs
index 250d7e7..7b91585 100644
--- a/src/HSVIS/Typecheck/Solve.hs
+++ b/src/HSVIS/Typecheck/Solve.hs
@@ -84,7 +84,7 @@ solveConstraints reduce frees subst detect size = \tupcs ->
   in trace ("[solver] Solving:" ++ concat ["\n- " ++ pretty a ++ "  ==  " ++ pretty b ++ "  {" ++ pretty r ++ "}" | Constr a b r <- cs]) $
      trace ("[solver] Result: (with " ++ show (length errs'') ++ " errors)" ++
               concat ["\n- " ++ show v ++ " = " ++ pretty t | (v, t) <- Map.assocs asg'] ++
-              "\n... errors: " ++ intercalate ", " (map summariseUE (toList errs'')))
+              "\n... errors: [" ++ intercalate ", " (map summariseUE (toList errs'')) ++ "]")
      (asg', errs'')
   where
     reduce' :: Constr t t -> (Bag (Constr v t), Bag (Constr t t))
@@ -92,14 +92,14 @@ solveConstraints reduce frees subst detect size = \tupcs ->
 
     loop :: Map v (Bag (RConstr t)) -> [(v, t)] -> (Bag (UnifyErr v t), Map v t)
     loop m eqlog = do
-      traceM $ "[solver] Step:" ++ concat
-                 [case toList rhss of
-                    [] -> "\n- " ++ show v ++ " <no RHSs>"
-                    RConstr t r : rest ->
-                      "\n- " ++ show v ++ " == " ++ pretty t ++ "  {" ++ pretty r ++ "}" ++
-                        concat ["\n  " ++ replicate (length (show v)) ' ' ++ " == " ++ pretty t' ++ "  {" ++ pretty r' ++ "}"
-                               | RConstr t' r' <- rest]
-                 | (v, rhss) <- Map.assocs m]
+      -- traceM $ "[solver] Step:" ++ concat
+      --            [case toList rhss of
+      --               [] -> "\n- " ++ show v ++ " <no RHSs>"
+      --               RConstr t r : rest ->
+      --                 "\n- " ++ show v ++ " == " ++ pretty t ++ "  {" ++ pretty r ++ "}" ++
+      --                   concat ["\n  " ++ replicate (length (show v)) ' ' ++ " == " ++ pretty t' ++ "  {" ++ pretty r' ++ "}"
+      --                          | RConstr t' r' <- rest]
+      --            | (v, rhss) <- Map.assocs m]
 
       m' <- Map.traverseWithKey
               (\v rhss ->
@@ -120,10 +120,10 @@ solveConstraints reduce frees subst detect size = \tupcs ->
 
       case msmallestvar of
         Nothing -> do
-          traceM $ "[solver] Log = [" ++ intercalate ", " [show v ++ " = " ++ pretty t | (v, t) <- eqlog] ++ "]"
+          -- traceM $ "[solver] Log = [" ++ intercalate ", " [show v ++ " = " ++ pretty t | (v, t) <- eqlog] ++ "]"
           return $ applyLog eqlog mempty
         Just (var, RConstr smallrhs _) -> do
-          traceM $ "[solver] Retiring " ++ show var ++ " = " ++ pretty smallrhs
+          -- traceM $ "[solver] Retiring " ++ show var ++ " = " ++ pretty smallrhs
           let (_, otherrhss) = bagPartition (guard . (== smallrhs) . rconType) (m' Map.! var)
           let (newcs, errs) = foldMap (reduce' . unsplitConstr smallrhs) (dedupRCs (toList otherrhss))
           (fmap constrUnequal errs, ())  -- write the errors