typechecker

3 files changed, 285 insertions, 190 deletions

diff --git a/src/HSVIS/AST.hs b/src/HSVIS/AST.hs
index 91e08eb..63594bc 100644
--- a/src/HSVIS/AST.hs
+++ b/src/HSVIS/AST.hs
@@ -9,11 +9,11 @@
 {-# LANGUAGE ConstrainedClassMethods #-}
 module HSVIS.AST where
 
-import Data.Bifunctor (bimap, first, second)
+-- import Data.Bifunctor (bimap, first, second)
 import qualified Data.Kind as DK
 import Data.List (intersperse)
 import Data.List.NonEmpty (NonEmpty)
-import Data.Proxy
+-- import Data.Proxy
 
 import HSVIS.Pretty
 
@@ -32,30 +32,30 @@ class HasExt f where
   type HasECon f :: Bool
   type ContainsData f :: [ASTType]
   extOf :: HasXField f ~ 'True => f s -> X f s
-  extMap :: Proxy f -> Proxy s1 -> Proxy s2
-         -> XMapperTelescope (f ': ContainsData f) s1 s2
-              (EMapperTelescope (f ': ContainsData f) s1 s2
-                (f s1 -> f s2))
+  -- extMap :: Proxy f -> Proxy s1 -> Proxy s2
+  --        -> XMapperTelescope (f ': ContainsData f) s1 s2
+  --             (EMapperTelescope (f ': ContainsData f) s1 s2
+  --               (f s1 -> f s2))
 
 type family If c a b where
   If 'True a b = a
   If 'False a b = b
 
-type family XMapperTelescope fs s1 s2 a where
-  XMapperTelescope '[] s1 s2 a = a
-  XMapperTelescope (f ': fs) s1 s2 a =
-    If (HasXField f)
-       ((X f s1 -> X f s2) -> XMapperTelescope fs s1 s2 a)
-       (XMapperTelescope fs s1 s2 a)
+-- type family XMapperTelescope fs s1 s2 a where
+--   XMapperTelescope '[] s1 s2 a = a
+--   XMapperTelescope (f ': fs) s1 s2 a =
+--     If (HasXField f)
+--        ((X f s1 -> X f s2) -> XMapperTelescope fs s1 s2 a)
+--        (XMapperTelescope fs s1 s2 a)
 
-type family EMapperTelescope fs s1 s2 a where
-  EMapperTelescope '[] s1 s2 a = a
-  EMapperTelescope (f ': fs) s1 s2 a =
-    If (HasECon f)
-       (If (HasXField f) (X f s1 -> E f s1 -> f s2)
-                         (E f s1 -> f s2)
-        -> EMapperTelescope fs s1 s2 a)
-       (EMapperTelescope fs s1 s2 a)
+-- type family EMapperTelescope fs s1 s2 a where
+--   EMapperTelescope '[] s1 s2 a = a
+--   EMapperTelescope (f ': fs) s1 s2 a =
+--     If (HasECon f)
+--        (If (HasXField f) (X f s1 -> E f s1 -> f s2)
+--                          (E f s1 -> f s2)
+--         -> EMapperTelescope fs s1 s2 a)
+--        (EMapperTelescope fs s1 s2 a)
 
 
 newtype Name = Name String
@@ -64,16 +64,19 @@ newtype Name = Name String
 data Program s = Program [DataDef s] [FunDef s]
 deriving instance (Show (DataDef s), Show (FunDef s)) => Show (Program s)
 
-data DataDef s = DataDef (X DataDef s) Name [(X Type s, Name)] [(Name, [Type s])]
-deriving instance (Show (X DataDef s), Show (X Type s), Show (E Type s)) => Show (DataDef s)
+data DataDef s = DataDef (X DataDef s) Name [(X Type s, Name)] [(Name, [DataField s])]
+deriving instance (Show (X DataDef s), Show (DataField s), Show (X Type s)) => Show (DataDef s)
+
+data DataField s = DataField (X DataField s) (Type s)
+deriving instance (Show (X DataField s), Show (X Type s), Show (E Type s)) => Show (DataField s)
 
 data FunDef s = FunDef (X FunDef s) Name (TypeSig s) (NonEmpty (FunEq s))
 deriving instance (Show (X FunDef s), Show (TypeSig s), Show (FunEq s)) => Show (FunDef s)
 
 data TypeSig s
-  = TypeSig (Type s)
-  | TypeSigExt !(E TypeSig s)
-deriving instance (Show (E TypeSig s), Show (Type s)) => Show (TypeSig s)
+  = TypeSig (X TypeSig s) (Type s)
+  | TypeSigExt (X TypeSig s) !(E TypeSig s)
+deriving instance (Show (X TypeSig s), Show (E TypeSig s), Show (Type s)) => Show (TypeSig s)
 
 data FunEq s = FunEq (X FunEq s) Name [Pattern s] (RHS s)
 deriving instance (Show (X FunEq s), Show (Pattern s), Show (RHS s)) => Show (FunEq s)
@@ -171,7 +174,7 @@ instance (Pretty (X Type s), Pretty (E Type s)) => Pretty (DataDef s) where
                    | (k, n) <- vars]
     . showString " = "
     . foldr (.) id (intersperse (showString " | ")
-                      [prettysPrec 11 cname . foldr (.) id [showString " " . prettysPrec 11 t | t <- fields]
+                      [prettysPrec 11 cname . foldr (.) id [showString " " . prettysPrec 11 t | DataField _ t <- fields]
                       | (cname, fields) <- cons])
 
 instance Pretty Operator where
@@ -188,38 +191,47 @@ instance Pretty Operator where
 instance HasExt DataDef where
   type HasXField DataDef = 'True
   type HasECon DataDef = 'False
-  type ContainsData DataDef = '[Type]
+  type ContainsData DataDef = '[DataField, Type]
   extOf (DataDef x _ _ _) = x
-  extMap _ ps1 ps2 fdd fty gty (DataDef x n ps cs) =
-    DataDef (fdd x) n (map (first fty) ps) (map (second (map (extMap (Proxy @Type) ps1 ps2 fty gty))) cs)
+  -- extMap _ ps1 ps2 fdd fdf fty gty (DataDef x n ps cs) =
+  --   DataDef (fdd x) n (map (first fty) ps)
+  --           (map (second (map (extMap (Proxy @DataField) ps1 ps2 fdf fty gty))) cs)
+
+instance HasExt DataField where
+  type HasXField DataField = 'True
+  type HasECon DataField = 'False
+  type ContainsData DataField = '[Type]
+  extOf (DataField x _) = x
+  -- extMap _ ps1 ps2 fdf fty gty (DataField x t) =
+  --   DataField (fdf x) (extMap (Proxy @Type) ps1 ps2 fty gty t)
 
 instance HasExt FunDef where
   type HasXField FunDef = 'True
   type HasECon FunDef = 'False
   type ContainsData FunDef = '[TypeSig, FunEq, Type, Pattern, RHS, Expr]
   extOf (FunDef x _ _ _) = x
-  extMap _ ps1 ps2 ffd ffe fty fpa frh fex gts gty (FunDef x n sig es) =
-    FunDef (ffd x) n
-           (extMap (Proxy @TypeSig) ps1 ps2 fty gts gty sig)
-           (fmap (extMap (Proxy @FunEq) ps1 ps2 ffe ffd fty fpa frh fex gts gty) es)
+  -- extMap _ ps1 ps2 ffd fts ffe fty fpa frh fex gts gty (FunDef x n sig es) =
+  --   FunDef (ffd x) n
+  --          (extMap (Proxy @TypeSig) ps1 ps2 fty gts gty sig)
+  --          (fmap (extMap (Proxy @FunEq) ps1 ps2 ffe ffd fty fpa frh fex gts gty) es)
 
 instance HasExt TypeSig where
-  type HasXField TypeSig = 'False
+  type HasXField TypeSig = 'True
   type HasECon TypeSig = 'True
   type ContainsData TypeSig = '[Type]
   extOf _ = undefined
-  extMap _ ps1 ps2 fty _   gty (TypeSig ty) =
-    TypeSig (extMap (Proxy @Type) ps1 ps2 fty gty ty)
-  extMap _ _   _   _   gts _   (TypeSigExt e) = gts e
+  -- extMap _ ps1 ps2 fty _   gty (TypeSig x ty) =
+  --   TypeSig (extMap (Proxy @Type) ps1 ps2 fty gty ty)
+  -- extMap _ _   _   _   gts _   (TypeSigExt x e) = gts e
 
 instance HasExt FunEq where
   type HasXField FunEq = 'True
   type HasECon FunEq = 'False
   type ContainsData FunEq = '[FunDef, TypeSig, Type, Pattern, RHS, Expr]
   extOf (FunEq x _ _ _) = x
-  extMap _ ps1 ps2 ffe ffd fty fpa frh fex gts gty (FunEq x n ps rhs) =
-    FunEq (ffe x) n (map (extMap (Proxy @Pattern) ps1 ps2 fpa) ps)
-          (extMap (Proxy @RHS) ps1 ps2 frh ffd ffe fty fpa fex gts gty rhs)
+  -- extMap _ ps1 ps2 ffe ffd fty fpa frh fex gts gty (FunEq x n ps rhs) =
+  --   FunEq (ffe x) n (map (extMap (Proxy @Pattern) ps1 ps2 fpa) ps)
+  --         (extMap (Proxy @RHS) ps1 ps2 frh ffd ffe fty fpa fex gts gty rhs)
 
 instance HasExt Kind where
   type HasXField Kind = 'True
@@ -228,9 +240,9 @@ instance HasExt Kind where
   extOf (KType x) = x
   extOf (KFun x _ _) = x
   extOf (KExt x _) = x
-  extMap _ _   _   f _ (KType x) = KType (f x)
-  extMap p ps1 ps2 f g (KFun x a b) = KFun (f x) (extMap p ps1 ps2 f g a) (extMap p ps1 ps2 f g b)
-  extMap _ _   _   _ g (KExt x a) = g x a
+  -- extMap _ _   _   f _ (KType x) = KType (f x)
+  -- extMap p ps1 ps2 f g (KFun x a b) = KFun (f x) (extMap p ps1 ps2 f g a) (extMap p ps1 ps2 f g b)
+  -- extMap _ _   _   _ g (KExt x a) = g x a
 
 instance HasExt Type where
   type HasXField Type = 'True
@@ -245,14 +257,14 @@ instance HasExt Type where
   extOf (TForall x _ _) = x
   extOf (TExt x _) = x
 
-  extMap p ps1 ps2 f g (TApp x a b) = TApp (f x) (extMap p ps1 ps2 f g a) (map (extMap p ps1 ps2 f g) b)
-  extMap p ps1 ps2 f g (TTup x as) = TTup (f x) (map (extMap p ps1 ps2 f g) as)
-  extMap p ps1 ps2 f g (TList x a) = TList (f x) (extMap p ps1 ps2 f g a)
-  extMap p ps1 ps2 f g (TFun x a b) = TFun (f x) (extMap p ps1 ps2 f g a) (extMap p ps1 ps2 f g b)
-  extMap _ _   _   f _ (TCon x n) = TCon (f x) n
-  extMap _ _   _   f _ (TVar x n) = TVar (f x) n
-  extMap p ps1 ps2 f g (TForall x n a) = TForall (f x) n (extMap p ps1 ps2 f g a)
-  extMap _ _   _   _ g (TExt x e) = g x e
+  -- extMap p ps1 ps2 f g (TApp x a b) = TApp (f x) (extMap p ps1 ps2 f g a) (map (extMap p ps1 ps2 f g) b)
+  -- extMap p ps1 ps2 f g (TTup x as) = TTup (f x) (map (extMap p ps1 ps2 f g) as)
+  -- extMap p ps1 ps2 f g (TList x a) = TList (f x) (extMap p ps1 ps2 f g a)
+  -- extMap p ps1 ps2 f g (TFun x a b) = TFun (f x) (extMap p ps1 ps2 f g a) (extMap p ps1 ps2 f g b)
+  -- extMap _ _   _   f _ (TCon x n) = TCon (f x) n
+  -- extMap _ _   _   f _ (TVar x n) = TVar (f x) n
+  -- extMap p ps1 ps2 f g (TForall x n a) = TForall (f x) n (extMap p ps1 ps2 f g a)
+  -- extMap _ _   _   _ g (TExt x e) = g x e
 
 instance HasExt Pattern where
   type HasXField Pattern = 'True
@@ -266,13 +278,13 @@ instance HasExt Pattern where
   extOf (PList x _) = x
   extOf (PTup x _) = x
 
-  extMap _ _   _   f (PWildcard x) = PWildcard (f x)
-  extMap _ _   _   f (PVar x n) = PVar (f x) n
-  extMap p ps1 ps2 f (PAs x n a) = PAs (f x) n (extMap p ps1 ps2 f a)
-  extMap p ps1 ps2 f (PCon x n as) = PCon (f x) n (map (extMap p ps1 ps2 f) as)
-  extMap p ps1 ps2 f (POp x a n b) = POp (f x) (extMap p ps1 ps2 f a) n (extMap p ps1 ps2 f b)
-  extMap p ps1 ps2 f (PList x as) = PList (f x) (map (extMap p ps1 ps2 f) as)
-  extMap p ps1 ps2 f (PTup x as) = PTup (f x) (map (extMap p ps1 ps2 f) as)
+  -- extMap _ _   _   f (PWildcard x) = PWildcard (f x)
+  -- extMap _ _   _   f (PVar x n) = PVar (f x) n
+  -- extMap p ps1 ps2 f (PAs x n a) = PAs (f x) n (extMap p ps1 ps2 f a)
+  -- extMap p ps1 ps2 f (PCon x n as) = PCon (f x) n (map (extMap p ps1 ps2 f) as)
+  -- extMap p ps1 ps2 f (POp x a n b) = POp (f x) (extMap p ps1 ps2 f a) n (extMap p ps1 ps2 f b)
+  -- extMap p ps1 ps2 f (PList x as) = PList (f x) (map (extMap p ps1 ps2 f) as)
+  -- extMap p ps1 ps2 f (PTup x as) = PTup (f x) (map (extMap p ps1 ps2 f) as)
 
 instance HasExt RHS where
   type HasXField RHS = 'True
@@ -281,13 +293,13 @@ instance HasExt RHS where
   extOf (Guarded x _) = x
   extOf (Plain x _) = x
 
-  extMap _ ps1 ps2 frh ffd ffe fty fpa fex gts gty (Guarded x l) =
-    Guarded (frh x)
-            (map (bimap (extMap (Proxy @Expr) ps1 ps2 fex ffd ffe fty fpa frh gts gty)
-                        (extMap (Proxy @Expr) ps1 ps2 fex ffd ffe fty fpa frh gts gty))
-                 l)
-  extMap _ ps1 ps2 frh ffd ffe fty fpa fex gts gty (Plain x e) =
-    Plain (frh x) (extMap (Proxy @Expr) ps1 ps2 fex ffd ffe fty fpa frh gts gty e)
+  -- extMap _ ps1 ps2 frh ffd ffe fty fpa fex gts gty (Guarded x l) =
+  --   Guarded (frh x)
+  --           (map (bimap (extMap (Proxy @Expr) ps1 ps2 fex ffd ffe fty fpa frh gts gty)
+  --                       (extMap (Proxy @Expr) ps1 ps2 fex ffd ffe fty fpa frh gts gty))
+  --                l)
+  -- extMap _ ps1 ps2 frh ffd ffe fty fpa fex gts gty (Plain x e) =
+  --   Plain (frh x) (extMap (Proxy @Expr) ps1 ps2 fex ffd ffe fty fpa frh gts gty e)
 
 instance HasExt Expr where
   type HasXField Expr = 'True
@@ -305,18 +317,18 @@ instance HasExt Expr where
   extOf (ELet x _ _) = x
   extOf (EError x) = x
 
-  extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty = \case
-    ELit x l -> ELit (fex x) l
-    EVar x n -> EVar (fex x) n
-    ECon x n -> ECon (fex x) n
-    EList x es -> EList (fex x) (map (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty) es)
-    ETup x es -> ETup (fex x) (map (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty) es)
-    EApp x a es -> EApp (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a) (map (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty) es)
-    EOp x a n b -> EOp (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a) n (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty b)
-    EIf x a b c -> EIf (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty b) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty c)
-    ECase x a l -> ECase (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a)
-                         (map (bimap (extMap (Proxy @Pattern) ps1 ps2 fpa)
-                                     (extMap (Proxy @RHS) ps1 ps2 frh ffd ffe fty fpa fex gts gty))
-                              l)
-    ELet x as b -> ELet (fex x) (map (extMap (Proxy @FunDef) ps1 ps2 ffd ffe fty fpa frh fex gts gty) as) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty b)
-    EError x -> EError (fex x)
+  -- extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty = \case
+  --   ELit x l -> ELit (fex x) l
+  --   EVar x n -> EVar (fex x) n
+  --   ECon x n -> ECon (fex x) n
+  --   EList x es -> EList (fex x) (map (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty) es)
+  --   ETup x es -> ETup (fex x) (map (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty) es)
+  --   EApp x a es -> EApp (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a) (map (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty) es)
+  --   EOp x a n b -> EOp (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a) n (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty b)
+  --   EIf x a b c -> EIf (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty b) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty c)
+  --   ECase x a l -> ECase (fex x) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty a)
+  --                        (map (bimap (extMap (Proxy @Pattern) ps1 ps2 fpa)
+  --                                    (extMap (Proxy @RHS) ps1 ps2 frh ffd ffe fty fpa fex gts gty))
+  --                             l)
+  --   ELet x as b -> ELet (fex x) (map (extMap (Proxy @FunDef) ps1 ps2 ffd ffe fty fpa frh fex gts gty) as) (extMap p ps1 ps2 fex ffd ffe fty fpa frh gts gty b)
+  --   EError x -> EError (fex x)
diff --git a/src/HSVIS/Parser.hs b/src/HSVIS/Parser.hs
index e89c679..bea0524 100644
--- a/src/HSVIS/Parser.hs
+++ b/src/HSVIS/Parser.hs
@@ -30,6 +30,7 @@ import Control.Monad.Chronicle
 import Control.Monad.Reader
 import Control.Monad.State.Lazy
 import Data.Char
+import Data.Bifunctor (second)
 import Data.Either (partitionEithers)
 import Data.Foldable
 import Data.List.NonEmpty (NonEmpty(..))
@@ -49,7 +50,9 @@ import HSVIS.Pretty
 data StageParsed
 
 type instance X DataDef StageParsed = Range
+type instance X DataField StageParsed = ()
 type instance X FunDef  StageParsed = Range
+type instance X TypeSig StageParsed = ()
 type instance X FunEq   StageParsed = Range
 type instance X Type    StageParsed = Range
 type instance X Pattern StageParsed = Range
@@ -233,7 +236,7 @@ pDataDef0 = do
         params <- famany (inlineWhite >> ranged (pIdentifier0 InBlock Lowercase WCBacktrack))
         cons <- pDatacons "="
         pos2 <- gets psCur
-        return [DataDef (Range pos1 pos2) name params cons]
+        return [DataDef (Range pos1 pos2) name params (map (second (map (DataField ()))) cons)]
   where
     pDatacons :: String -> IParser [(Name, [PType])]
     pDatacons leader = do
@@ -262,20 +265,20 @@ pFunDef0 =
               clauses <- concat <$> famany (pFunEq (Continue name))
               let clauses' = clause1 :| clauses1 ++ clauses
               let rng = sigrange <> foldMapne extOf clauses'
-              return [FunDef rng name (TypeSig typ) clauses']
+              return [FunDef rng name (TypeSig () typ) clauses']
             _ -> do
               pos <- gets psCur
               raise Error $ "Expected function equation for " ++ pretty name ++
                             " after type signature"
               let rng = Range pos pos
-              return [FunDef sigrange name (TypeSig typ)
+              return [FunDef sigrange name (TypeSig () typ)
                              (FunEq rng name [] (Plain rng (EError rng)) :| [])]
     ,do pFunEq FirstLine >>= \case
           clause1@(FunEq _ name _ _) : clauses1 -> noFail $ do
             clauses <- concat <$> famany (pFunEq (Continue name))
             let clauses' = clause1 :| clauses1 ++ clauses
             let rng = foldMapne extOf clauses'
-            return [FunDef rng name (TypeSigExt NoTypeSig) clauses']
+            return [FunDef rng name (TypeSigExt () NoTypeSig) clauses']
           [] -> faempty]
 
 -- | Given the name from the type signature or a previous clause, if any.
diff --git a/src/HSVIS/Typecheck.hs b/src/HSVIS/Typecheck.hs
index 2dd103f..1e46a99 100644
--- a/src/HSVIS/Typecheck.hs
+++ b/src/HSVIS/Typecheck.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE EmptyDataDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -7,40 +8,28 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE GADTs #-}
-
-
-
-{-# OPTIONS -Wno-unused-top-binds #-}
-{-# OPTIONS -Wno-unused-imports #-}
-{-# LANGUAGE DataKinds #-}
-
-
-
 module HSVIS.Typecheck (
   StageTyped,
   typecheck,
   -- * Typed AST synonyms
-  -- TProgram, TDataDef, TFunDef, TFunEq, TKind, TType, TPattern, TRHS, TExpr,
+  TProgram, TDataDef, TDataField, TFunDef, TFunEq, TKind, TType, TPattern, TRHS, TExpr,
 ) where
 
 import Control.Monad
 import Data.Bifunctor (first, second, bimap)
 import Data.Foldable (toList)
-import Data.List (find, inits)
+import Data.List (inits)
 import Data.Map.Strict (Map)
 import Data.Maybe (fromMaybe)
-import Data.Monoid (Ap(..))
 import qualified Data.Map.Strict as Map
 import Data.Tuple (swap)
 import Data.Semigroup (First(..))
 import Data.Set (Set)
 import qualified Data.Set as Set
-import GHC.Stack
 
 import Debug.Trace
 
 import Data.Bag
-import Data.List.NonEmpty.Util
 import Data.Map.Monoidal (MMap(..))
 import qualified Data.Map.Monoidal as MMap
 import HSVIS.AST
@@ -53,13 +42,15 @@ import HSVIS.Typecheck.Solve
 data StageTC
 
 type instance X DataDef StageTC = CKind
-type instance X FunDef  StageTC = CType
+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 Pattern StageTC = CType
+type instance X Pattern StageTC = (Range, CType)
 type instance X RHS     StageTC = CType
-type instance X Expr    StageTC = CType
+type instance X Expr    StageTC = (Range, CType)
 
 data instance E Type StageTC = TUniVar Int deriving (Show, Eq, Ord)
 data instance E Kind StageTC = KUniVar Int deriving (Show, Eq, Ord)
@@ -67,6 +58,7 @@ data instance E TypeSig StageTC deriving (Show)
 
 type CProgram = Program StageTC
 type CDataDef = DataDef StageTC
+type CDataField = DataField StageTC
 type CFunDef  = FunDef  StageTC
 type CFunEq   = FunEq   StageTC
 type CKind    = Kind    StageTC
@@ -78,7 +70,9 @@ type CExpr    = Expr    StageTC
 data StageTyped
 
 type instance X DataDef StageTyped = TKind
-type instance X FunDef  StageTyped = TType
+type instance X DataField StageTyped = Range
+type instance X FunDef  StageTyped = ()
+type instance X TypeSig StageTyped = ()
 type instance X FunEq   StageTyped = ()
 type instance X Kind    StageTyped = ()
 type instance X Type    StageTyped = TKind
@@ -92,6 +86,7 @@ data instance E TypeSig StageTyped deriving (Show)
 
 type TProgram = Program StageTyped
 type TDataDef = DataDef StageTyped
+type TDataField = DataField StageTyped
 type TFunDef  = FunDef  StageTyped
 type TFunEq   = FunEq   StageTyped
 type TKind    = Kind    StageTyped
@@ -251,7 +246,7 @@ tcTop :: PProgram -> TCM TProgram
 tcTop prog = do
   (cs, prog') <- collectConstraints Just (tcProgram prog)
   (subK, subT) <- solveConstrs cs
-  return $ finaliseProg (substProg subK subT prog')
+  finaliseProg (substProg subK subT prog')
 
 tcProgram :: PProgram -> TCM CProgram
 tcProgram (Program ddefs1 fdefs1) = do
@@ -301,9 +296,10 @@ kcDataDef (kd, parkinds) (DataDef _ name params cons) = do
   -- kind-check the constructors
   cons' <- scopeTEnv $ do
     modifyTEnv (Map.fromList (zip params' parkinds) <>)
-    forM cons $ \(cname, fieldtys) -> do
-      fieldtys' <- mapM (kcType KCTMNormal (Just (KType ()))) fieldtys
-      return (cname, fieldtys')
+    forM cons $ \(cname, fields) -> do
+      fields' <- forM fields $ \(DataField () t) ->
+        DataField (extOf t) <$> kcType KCTMNormal (Just (KType ())) t
+      return (cname, fields')
 
   return (DataDef kd name (zip parkinds params') cons')
 
@@ -311,7 +307,7 @@ 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)
-  in [(cname, InvCon tyvars resty fields) | (cname, fields) <- cons]
+  in [(cname, InvCon tyvars resty (map dataFieldType fields)) | (cname, fields) <- cons]
 
 promoteDownK :: Maybe CKind -> TCM CKind
 promoteDownK Nothing = genKUniVar
@@ -401,7 +397,7 @@ tcFunDefBlock fdefs = do
 
   -- take the actual found types for typechecking the body (and link them
   -- to the variables generated above)
-  let bound2 = map (\(FunDef ty n _ _) -> (n, ty)) defs'
+  let bound2 = map (\(FunDef _ n (TypeSig _ ty) _) -> (n, ty)) defs'
   forM_ (zip3 fdefs bound bound2) $ \(fdef, (_, tvar), (_, ty)) ->
     emit $ CEq ty tvar (extOf fdef)  -- which is expected/observed? which range? /shrug/
 
@@ -412,8 +408,8 @@ tcFunDef (FunDef rng name msig eqs) = do
   when (not $ allEq (fmap (length . funeqPats) eqs)) $
     raise SError rng "Function equations have differing numbers of arguments"
 
-  typ <- case msig of
-    TypeSig sig -> do
+  (typ, msigrng) <- case msig of
+    TypeSig _ sig -> do
       (typ, freetvars) <- kcType KCTMOpen (Just (KType ())) sig
       TODO -- We need to check that these free type variables do not escape.
            -- Perhaps with levels on unification variables? Associate a level
@@ -421,14 +417,15 @@ tcFunDef (FunDef rng name msig eqs) = do
            -- passing below a forall.
            -- But how do we deal with functions without a type signature
            -- anyway? We should be able to infer a polymorphic type for them.
-      return $ foldr (\(n, k) -> TForall k n) typ (Map.assocs freetvars)
-    TypeSigExt NoTypeSig -> genUniVar (KType ())
+      return (foldr (\(n, k) -> TForall k n) typ (Map.assocs freetvars)
+             ,Just (extOf sig))
+    TypeSigExt _ NoTypeSig -> (,Nothing) <$> genUniVar (KType ())
 
   eqs' <- scopeVEnv $ do
     modifyVEnv (Map.insert name typ)  -- allow function to be recursive
     mapM (tcFunEq typ) eqs
 
-  return (FunDef typ name (TypeSig typ) eqs')
+  return (FunDef rng name (TypeSig msigrng typ) eqs')
 
 tcFunEq :: CType -> PFunEq -> TCM CFunEq
 tcFunEq down (FunEq rng name pats rhs) = do
@@ -442,11 +439,14 @@ tcFunEq down (FunEq rng name pats rhs) = do
 -- | Brings the bound variables in scope
 tcPattern :: CType -> PPattern -> TCM CPattern
 tcPattern down = \case
-  PWildcard _ -> return $ PWildcard down
+  PWildcard rng -> return $ PWildcard (rng, down)
 
-  PVar _ n -> modifyVEnv (Map.insert n down) >> return (PVar down n)
+  PVar rng n -> modifyVEnv (Map.insert n down) >> return (PVar (rng, down) n)
 
-  PAs _ n p -> modifyVEnv (Map.insert n down) >> tcPattern down p
+  PAs rng n p -> do
+    modifyVEnv (Map.insert n down)
+    p' <- tcPattern down p
+    return $ PAs (rng, snd (extOf p')) n p'
 
   PCon rng n ps ->
     getInvCon n >>= \case
@@ -455,10 +455,10 @@ tcPattern down = \case
         let match' = substType mempty mempty unisub match
             fields' = map (substType mempty mempty unisub) fields
         emit $ CEq down match' rng
-        PCon match' n <$> zipWithM tcPattern fields' ps
+        PCon (rng, match') n <$> zipWithM tcPattern fields' ps
       Nothing -> do
         raise SError rng $ "Constructor not in scope: " ++ pretty n
-        return (PWildcard down)
+        return (PWildcard (rng, down))
 
   POp rng p1 op p2 ->
     case op of
@@ -468,27 +468,27 @@ tcPattern down = \case
         emit $ CEq down listty rng
         p1' <- tcPattern eltty p1
         p2' <- tcPattern listty p2
-        return (POp listty p1' OCons p2')
+        return (POp (rng, listty) p1' OCons p2')
       _ -> do
         raise SError rng $ "Operator is not a constructor: " ++ pretty op
-        return (PWildcard down)
+        return (PWildcard (rng, down))
 
   PList rng ps -> do
     eltty <- genUniVar (KType ())
     let listty = TList (KType ()) eltty
     emit $ CEq down listty rng
-    PList listty <$> mapM (tcPattern eltty) ps
+    PList (rng, listty) <$> mapM (tcPattern eltty) ps
 
   PTup rng ps -> do
     ts <- mapM (\_ -> genUniVar (KType ())) ps
     emit $ CEq down (TTup (KType ()) ts) rng
-    PTup (TTup (KType ()) ts) <$> zipWithM tcPattern ts ps
+    PTup (rng, TTup (KType ()) ts) <$> zipWithM tcPattern ts ps
 
 tcRHS :: CType -> PRHS -> TCM CRHS
 tcRHS _ (Guarded _ _) = error "typecheck: Guards not yet supported"
 tcRHS down (Plain _ e) = do
   e' <- tcExpr down e
-  return $ Plain (extOf e') e'
+  return $ Plain (snd (extOf e')) e'
 
 tcExpr :: CType -> PExpr -> TCM CExpr
 tcExpr down = \case
@@ -499,34 +499,34 @@ tcExpr down = \case
                LChar{} -> TCon (KType ()) (Name "Char")
                LString{} -> TList (KType ()) (TCon (KType ()) (Name "Char"))
     emit $ CEq down ty rng
-    return (ELit ty lit)
+    return $ ELit (rng, ty) lit
 
   EVar rng n -> do
     ty <- getType' rng n
     emit $ CEq down ty rng
-    return $ EVar ty n
+    return $ EVar (rng, ty) n
 
   ECon rng n -> do
     ty <- getType' rng n
     emit $ CEq down ty rng
-    return $ EVar ty n
+    return $ EVar (rng, ty) n
 
   EList rng es -> do
     eltty <- genUniVar (KType ())
     let listty = TList (KType ()) eltty
     emit $ CEq down listty rng
-    EList listty <$> mapM (tcExpr listty) es
+    EList (rng, listty) <$> mapM (tcExpr listty) es
 
   ETup rng es -> do
     ts <- mapM (\_ -> genUniVar (KType ())) es
     emit $ CEq down (TTup (KType ()) ts) rng
-    ETup (TTup (KType ()) ts) <$> zipWithM tcExpr ts es
+    ETup (rng, TTup (KType ()) ts) <$> zipWithM tcExpr ts es
 
-  EApp _ e1 es -> do
+  EApp rng e1 es -> do
     argtys <- mapM (\_ -> genUniVar (KType ())) es
     let funty = foldr (TFun (KType ())) down argtys
-    EApp funty <$> tcExpr funty e1
-               <*> zipWithM tcExpr argtys es
+    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
@@ -548,31 +548,31 @@ tcExpr down = \case
     emit $ CEq down rty rng
     e1' <- tcExpr aty1 e1
     e2' <- tcExpr aty2 e2
-    return (EOp rty e1' op e2')
+    return (EOp (rng, rty) e1' op e2')
 
-  EIf _ e1 e2 e3 -> do
+  EIf rng e1 e2 e3 -> do
     e1' <- tcExpr (TCon (KType ()) (Name "Bool")) e1
     e2' <- tcExpr down e2
     e3' <- tcExpr down e3
-    return (EIf down e1' e2' e3')
+    return (EIf (rng, down) e1' e2' e3')
 
-  ECase _ e1 alts -> do
+  ECase rng e1 alts -> do
     ty <- genUniVar (KType ())
     e1' <- tcExpr ty e1
     alts' <- forM alts $ \(pat, rhs) ->
       scopeVEnv $
         (,) <$> tcPattern ty pat <*> tcRHS down rhs
-    return $ ECase down e1' alts'
+    return $ ECase (rng, down) e1' alts'
 
-  ELet _ defs body -> do
+  ELet rng defs body -> do
     defs' <- tcFunDefBlock defs
-    let bound2 = map (\(FunDef ty n _ _) -> (n, ty)) defs'
+    let bound2 = map (\(FunDef _ n (TypeSig _ ty) _) -> (n, ty)) defs'
     scopeVEnv $ do
       modifyVEnv (Map.fromList bound2 <>)
       body' <- tcExpr down body
-      return $ ELet down defs' body'
+      return $ ELet (rng, down) defs' body'
 
-  EError _ -> return $ EError down
+  EError rng -> return $ EError (rng, down)
 
 unfoldFunTy :: Range -> Int -> CType -> TCM ([CType], CType)
 unfoldFunTy _ n t | n <= 0 = return ([], t)
@@ -706,70 +706,65 @@ partitionConstrs = foldMap $ \case CEq t1 t2 r -> (pure (t1, t2, r), mempty)
 -- - an instantiation map for type unification variables (Map Int CType)
 -- - an instantiation map for type variables (Map Name CType)
 
-substProg :: HasCallStack
-          => Map Int CKind -> Map Int CType -> CProgram -> CProgram
+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 :: HasCallStack
-          => Map Int CKind -> Map Int CType -> CDataDef -> CDataDef
+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)
-          (map (second (map (substType mk mt mempty))) cons)
+          (map (second (map (substDataField mk mt))) cons)
+
+substDataField :: Map Int CKind -> Map Int CType -> CDataField -> CDataField
+substDataField mk mt (DataField rng t) = DataField rng (substType mk mt mempty t)
 
-substFdef :: HasCallStack
-          => Map Int CKind -> Map Int CType -> CFunDef -> CFunDef
-substFdef mk mt (FunDef t n (TypeSig sig) eqs) =
-  FunDef (substType mk mt mempty t) n
-         (TypeSig (substType mk mt mempty sig))
+substFdef :: Map Int CKind -> Map Int CType -> CFunDef -> CFunDef
+substFdef mk mt (FunDef rng n (TypeSig sigrng sig) eqs) =
+  FunDef rng n
+         (TypeSig sigrng (substType mk mt mempty sig))
          (fmap (substFunEq mk mt) eqs)
 
-substFunEq :: HasCallStack
-           => Map Int CKind -> Map Int CType -> CFunEq -> CFunEq
+substFunEq :: Map Int CKind -> Map Int CType -> CFunEq -> CFunEq
 substFunEq mk mt (FunEq () n ps rhs) =
   FunEq () n
         (map (substPattern mk mt) ps)
         (substRHS mk mt rhs)
 
-substRHS :: HasCallStack
-         => Map Int CKind -> Map Int CType -> CRHS -> CRHS
+substRHS :: Map Int CKind -> Map Int CType -> CRHS -> CRHS
 substRHS _  _  (Guarded _ _) = error "typecheck: guards unsupported"
 substRHS mk mt (Plain t e) = Plain (substType mk mt mempty t) (substExpr mk mt e)
 
-substPattern :: HasCallStack
-             => Map Int CKind -> Map Int CType -> CPattern -> CPattern
+substPattern :: Map Int CKind -> Map Int CType -> CPattern -> CPattern
 substPattern mk mt = go
   where
-    go (PWildcard t) = PWildcard (goType t)
-    go (PVar t n) = PVar (goType t) n
-    go (PAs t n p) = PAs (goType t) n (go p)
-    go (PCon t n ps) = PCon (goType t) n (map go ps)
-    go (POp t p1 op p2) = POp (goType t) (go p1) op (go p2)
-    go (PList t ps) = PList (goType t) (map go ps)
-    go (PTup t ps) = PTup (goType t) (map go ps)
-
-    goType = substType mk mt mempty
-
-substExpr :: HasCallStack
-          => Map Int CKind -> Map Int CType -> CExpr -> CExpr
+    go (PWildcard e) = PWildcard (goExt e)
+    go (PVar e n) = PVar (goExt e) n
+    go (PAs e n p) = PAs (goExt e) n (go p)
+    go (PCon e n ps) = PCon (goExt e) n (map go ps)
+    go (POp e p1 op p2) = POp (goExt e) (go p1) op (go p2)
+    go (PList e ps) = PList (goExt e) (map go ps)
+    go (PTup e ps) = PTup (goExt e) (map go ps)
+
+    goExt (rng, t) = (rng, substType mk mt mempty t)
+
+substExpr :: Map Int CKind -> Map Int CType -> CExpr -> CExpr
 substExpr mk mt = go
   where
-    go (ELit t lit) = ELit (goType t) lit
-    go (EVar t n) = EVar (goType t) n
-    go (ECon t n) = ECon (goType t) n
-    go (EList t es) = EList (goType t) (map go es)
-    go (ETup t es) = ETup (goType t) (map go es)
-    go (EApp t e1 es) = EApp (goType t) (go e1) (map go es)
-    go (EOp t e1 op e2) = EOp (goType t) (go e1) op (go e2)
-    go (EIf t e1 e2 e3) = EIf (goType t) (go e1) (go e2) (go e3)
-    go (ECase t e1 alts) = ECase (goType t) (go e1) (map (bimap (substPattern mk mt) (substRHS mk mt)) alts)
-    go (ELet t defs body) = ELet (goType t) (map (substFdef mk mt) defs) (go body)
-    go (EError t) = EError (goType t)
-
-    goType = substType mk mt mempty
-
-substType :: HasCallStack
-          => Map Int CKind -> Map Int CType -> Map Name CType -> CType -> CType
+    go (ELit e lit) = ELit (goExt e) lit
+    go (EVar e n) = EVar (goExt e) n
+    go (ECon e n) = ECon (goExt e) n
+    go (EList e es) = EList (goExt e) (map go es)
+    go (ETup e es) = ETup (goExt e) (map go es)
+    go (EApp e e1 es) = EApp (goExt e) (go e1) (map go es)
+    go (EOp e e1 op e2) = EOp (goExt e) (go e1) op (go e2)
+    go (EIf e e1 e2 e3) = EIf (goExt e) (go e1) (go e2) (go e3)
+    go (ECase e e1 alts) = ECase (goExt e) (go e1) (map (bimap (substPattern mk mt) (substRHS mk mt)) alts)
+    go (ELet e defs body) = ELet (goExt e) (map (substFdef mk mt) defs) (go body)
+    go (EError e) = EError (goExt e)
+
+    goExt (rng, t) = (rng, substType mk mt mempty t)
+
+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)
@@ -783,8 +778,7 @@ substType mk mt mtv = go
 
     goKind = substKind mk
 
-substKind :: HasCallStack
-          => Map Int CKind -> CKind -> CKind
+substKind :: Map Int CKind -> CKind -> CKind
 substKind m = \case
   KType () -> KType ()
   KFun () k1 k2 -> KFun () (substKind m k1) (substKind m k2)
@@ -793,7 +787,84 @@ substKind m = \case
 -------------------- FINALISATION FUNCTIONS --------------------
 -- These report free type unification variables.
 
--- TODO the finalise* functions
+finaliseProg :: MonadRaise m => CProgram -> m TProgram
+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
+          <*> traverse (secondM (traverse finaliseDataField)) cons
+
+finaliseDataField :: MonadRaise m => CDataField -> m TDataField
+finaliseDataField (DataField rng t) = DataField rng <$> finaliseType rng t
+
+finaliseFdef :: MonadRaise m => CFunDef -> m TFunDef
+finaliseFdef (FunDef rng n (TypeSig msigrng sig) eqs) =
+  FunDef () n
+         <$> (TypeSig () <$> finaliseType (fromMaybe rng msigrng) sig)
+         <*> traverse finaliseFunEq eqs
+
+finaliseFunEq :: MonadRaise m => CFunEq -> m TFunEq
+finaliseFunEq (FunEq () n ps rhs) =
+  FunEq () n
+        <$> traverse finalisePattern ps
+        <*> finaliseRHS 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
+
+finalisePattern :: MonadRaise m => CPattern -> m TPattern
+finalisePattern = \case
+  PWildcard e -> PWildcard <$> goExt e
+  PVar e n -> PVar <$> goExt e <*> pure n
+  PAs e n p -> PAs <$> goExt e <*> pure n <*> finalisePattern p
+  PCon e n ps -> PCon <$> goExt e <*> pure n <*> traverse finalisePattern ps
+  POp e p1 op p2 -> POp <$> goExt e <*> finalisePattern p1 <*> pure op <*> finalisePattern p2
+  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
+
+finaliseExpr :: MonadRaise m => CExpr -> m TExpr
+finaliseExpr = \case
+  ELit e lit -> ELit <$> goExt e <*> pure lit
+  EVar e n -> EVar <$> goExt e <*> pure n
+  ECon e n -> ECon <$> goExt e <*> pure n
+  EList e es -> EList <$> goExt e <*> traverse finaliseExpr es
+  ETup e es -> ETup <$> goExt e <*> traverse finaliseExpr es
+  EApp e e1 es -> EApp <$> goExt e <*> finaliseExpr e1 <*> traverse finaliseExpr es
+  EOp e e1 op e2 -> EOp <$> goExt e <*> finaliseExpr e1 <*> pure op <*> finaliseExpr e2
+  EIf e e1 e2 e3 -> EIf <$> goExt e <*> finaliseExpr e1 <*> finaliseExpr e2 <*> finaliseExpr e3
+  ECase e e1 alts -> ECase <$> goExt e <*> finaliseExpr e1 <*> traverse (bimapM finalisePattern finaliseRHS) alts
+  ELet e defs body -> ELet <$> goExt e <*> traverse finaliseFdef defs <*> finaliseExpr body
+  EError e -> EError <$> goExt e
+  where
+    goExt (rng, t) = finaliseType rng t
+
+finaliseType :: MonadRaise m => Range -> CType -> m TType
+finaliseType rng toptype = go toptype
+  where
+    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 (TForall k n t) = TForall <$> finaliseKind k <*> pure n <*> go t
+    go t@(TExt k TUniVar{}) = do
+      raise SError rng $ "Ambiguous type unification variable " ++ pretty t ++ " in type: " ++ pretty toptype
+      TVar <$> finaliseKind k <*> pure (Name "$_error")
+
+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
+
+-------------------- END OF FINALISATION FUNCTIONS --------------------
 
 typeUniVars :: CType -> Set Int
 typeUniVars = \case
@@ -817,12 +888,21 @@ allEq l = case toList l of
             [] -> True
             x : xs -> all (== x) xs
 
-funeqPats :: FunEq t -> [Pattern t]
+funeqPats :: FunEq s -> [Pattern s]
 funeqPats (FunEq _ _ pats _) = pats
 
+dataFieldType :: DataField s -> Type s
+dataFieldType (DataField _ t) = t
+
 isCEqK :: Constr -> Maybe (CKind, CKind, Range)
 isCEqK (CEqK k1 k2 rng) = Just (k1, k2, rng)
 isCEqK _ = Nothing
 
-foldMapM :: (Applicative f, Monoid m, Foldable t) => (a -> f m) -> t a -> f m
-foldMapM f = getAp . foldMap (Ap . f)
+firstM :: Functor f => (a -> f b) -> (a, c) -> f (b, c)
+firstM f (x, y) = (,y) <$> f x
+
+secondM :: Functor f => (b -> f c) -> (a, b) -> f (a, c)
+secondM f (x, y) = (x,) <$> f y
+
+bimapM :: Applicative f => (a -> f b) -> (c -> f d) -> (a, c) -> f (b, d)
+bimapM f g (x, y) = (,) <$> f x <*> g y