diff --git a/app/Main.hs b/app/Main.hs
index 41e6a689..b97c0c21 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -17,7 +17,7 @@ main = do
   case mode of
     ModeHelp -> putStrLn $ usageInfo usage options
     ModeLSP -> do
-      _ <- runOnStdio "/Users/vince/Documents/gcl-vscode/server_log.txt"
+      _ <- runOnStdio "/Users/andy/Desktop/log.txt"
       return ()
     ModeDev -> do
       _ <- runOnPort port
diff --git a/src/GCL/Type.hs b/src/GCL/Type.hs
index 1a7ff5da..46cf5411 100644
--- a/src/GCL/Type.hs
+++ b/src/GCL/Type.hs
@@ -284,9 +284,9 @@ collectTypeDefns typeDefns = do
           let sub = Map.fromList . zip tyParamNames $ freshNames
           let sub' = Map.fromList . zip tyParamNames $ TMetaVar <$> freshNames <*> pure NoLoc
           let retTy = formTy (TData tyName' (locOf tyName')) (TMetaVar <$> tyParamNames <*> pure NoLoc)
-          let ty = subst sub' $ wrapTFunc (TVar <$> params <*> pure (locOf params)) retTy
+          let ty = subst sub' $ wrapTFunc params retTy
           -- Here, we collect the patterns.
-          let pat = (conName, subst sub' retTy, TVar <$> params <*> pure (locOf params)) -- TODO: This is likely incorrect because I just want to make things work now carelessly.
+          let pat = (conName, subst sub' retTy, params)
           modify (\(freshState, typeDefnInfos, origInfos, pats) -> (freshState, typeDefnInfos, origInfos, pat : pats))
           -- Here, we enter the world for infering kinds.
           (_kind, env'') <- inferKind (renameKindEnv sub env') ty
@@ -524,15 +524,15 @@ instance Elab Program where
 instance Elab Definition where
   elaborate (TypeDefn name args ctors loc) env = do
     let m = Set.fromList args
-    mapM_ (\(TypeDefnCtor _ ns) -> mapM_ (scopeCheck m) ns) ctors
+    mapM_ (\(TypeDefnCtor _ ts) -> mapM_ (scopeCheck m) ts) ctors
     ctors' <- mapM (\ctor -> do
                       (_, typed, _) <- elaborate ctor env
                       return typed
                    ) ctors
     return (Nothing, T.TypeDefn name args ctors' loc, mempty)
     where
-      scopeCheck :: MonadError TypeError m => Set.Set Name -> Name -> m ()
-      scopeCheck ns n = if Set.member n ns then return () else throwError $ NotInScope n
+      scopeCheck :: MonadError TypeError m => Set.Set Name -> Type -> m ()
+      scopeCheck ns t = mapM_ (\n -> if Set.member n ns then return () else throwError $ NotInScope n) (freeVars t)
   elaborate (FuncDefnSig name ty maybeExpr loc) env = do
     expr' <- mapM (\expr -> do
                     (_, typed, _) <- elaborate expr env
diff --git a/src/Syntax/Abstract/Types.hs b/src/Syntax/Abstract/Types.hs
index 20313d52..711ff1d7 100644
--- a/src/Syntax/Abstract/Types.hs
+++ b/src/Syntax/Abstract/Types.hs
@@ -42,7 +42,7 @@ data Definition =
     deriving (Eq, Show)
 
 -- constructor of type definition
-data TypeDefnCtor = TypeDefnCtor Name [Name]
+data TypeDefnCtor = TypeDefnCtor Name [Type]
   deriving (Eq, Show)
 
 --------------------------------------------------------------------------------
diff --git a/src/Syntax/Concrete/Instances/ToAbstract.hs b/src/Syntax/Concrete/Instances/ToAbstract.hs
index 1aedc047..6126babc 100644
--- a/src/Syntax/Concrete/Instances/ToAbstract.hs
+++ b/src/Syntax/Concrete/Instances/ToAbstract.hs
@@ -89,7 +89,9 @@ instance ToAbstract Definition [A.Definition] where
     return [A.FuncDefn name $ wrapLam args body']
 
 instance ToAbstract TypeDefnCtor A.TypeDefnCtor where
-  toAbstract (TypeDefnCtor c ns) = return $ A.TypeDefnCtor c ns
+  toAbstract (TypeDefnCtor c tys) = do
+    tys' <- mapM toAbstract tys
+    return $ A.TypeDefnCtor c tys'
 
 --------------------------------------------------------------------------------
 -- | Declaraion
diff --git a/src/Syntax/Concrete/Types.hs b/src/Syntax/Concrete/Types.hs
index 2d886952..416e4c4f 100644
--- a/src/Syntax/Concrete/Types.hs
+++ b/src/Syntax/Concrete/Types.hs
@@ -67,7 +67,7 @@ data Definition
   | FuncDefn Name [Name] (Token "=") Expr
   deriving (Eq, Show)
 
-data TypeDefnCtor = TypeDefnCtor Name [Name] deriving (Eq, Show)
+data TypeDefnCtor = TypeDefnCtor Name [Type] deriving (Eq, Show)
 
 --------------------------------------------------------------------------------
 -- | Declaration
diff --git a/src/Syntax/Parser.hs b/src/Syntax/Parser.hs
index 25056d17..0a0d3f51 100644
--- a/src/Syntax/Parser.hs
+++ b/src/Syntax/Parser.hs
@@ -267,7 +267,7 @@ definition = choice [try funcDefnSig, typeDefn, funcDefnF]
   typeDefn = TypeDefn <$> tokenData <*> upper <*> many lower <*> tokenEQ <*> sepByGuardBar typeDefnCtor
 
   typeDefnCtor :: Parser TypeDefnCtor
-  typeDefnCtor = TypeDefnCtor <$> upper <*> many identifier
+  typeDefnCtor = TypeDefnCtor <$> upper <*> many type'
 
 definitionBlock :: Parser DefinitionBlock
 definitionBlock = DefinitionBlock <$> tokenDeclOpen <*> sepByAlignmentOrSemi definition <*> tokenDeclClose
diff --git a/src/Syntax/Typed/Types.hs b/src/Syntax/Typed/Types.hs
index 91a45a91..b0042640 100644
--- a/src/Syntax/Typed/Types.hs
+++ b/src/Syntax/Typed/Types.hs
@@ -20,7 +20,7 @@ data Definition
   | FuncDefn Name Expr
   deriving (Eq, Show)
 
-data TypeDefnCtor = TypeDefnCtor Name [Name]
+data TypeDefnCtor = TypeDefnCtor Name [Type]
   deriving (Eq, Show)
 
 data Declaration