fix type of inductive names

src/Juvix/Syntax/MicroJuvix/InfoTable.hs

@@ -116,11 +116,11 @@ inductiveType v = do
   let ps = info ^. inductiveInfoDef . inductiveParameters
   return $
     foldr
-      (\p k -> ExpressionFunction (typeAbs (p ^. inductiveParamName) k))
-      (ExpressionUniverse (SmallUniverse (getLoc v)))
+      (\_ k -> uni --> k)
+      (smallUniverse (getLoc v))
       ps
   where
-    typeAbs var = Function (typeAbstraction Explicit var)
+    uni = smallUniverse (getLoc v)
 
 constructorArgTypes :: ConstructorInfo -> ([VarName], [Expression])
 constructorArgTypes i =

src/Juvix/Syntax/MicroJuvix/Language/Extra.hs

@@ -426,6 +426,19 @@ reachableModules = fst . run . runOutputList . evalState (mempty :: HashSet Name
           StatementInclude (Include inc) -> go inc
           _ -> return ()
 
+(-->) :: Expression -> Expression -> Expression
+(-->) a b =
+  ExpressionFunction
+    ( Function
+        ( FunctionParameter
+            { _paramName = Nothing,
+              _paramImplicit = Explicit,
+              _paramType = a
+            }
+        )
+        b
+    )
+
 -- | Assumes the given function has been type checked
 -- | NOTE: Registers the function *only* if the result is Type
 functionDefEval :: FunctionDef -> Maybe Expression
@@ -448,6 +461,7 @@ functionDefEval f = case f ^. funDefClauses of
           sparams <- mapM simpleExplicitParam nfirst
           let r' = foldFunType rest r
           return (sparams, r')
+        -- TODO normalize
         isUniverse :: Expression -> Bool
         isUniverse = \case
           ExpressionUniverse {} -> True

src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs

@@ -158,7 +158,7 @@ instance PrettyCode FunctionParameter where
       Just n -> do
         paramName' <- ppCode n
         paramType' <- ppCode _paramType
-        return $ implicitDelim _paramImplicit (paramName' <+> paramType')
+        return $ implicitDelim _paramImplicit (paramName' <+> kwColon <+> paramType')
 
 instance PrettyCode Function where
   ppCode (Function l r) = do

src/Juvix/Syntax/MicroJuvix/TypeChecker/Inference.hs

@@ -26,7 +26,6 @@ makeLenses ''MatchError
 data Inference m a where
   MatchTypes :: Expression -> Expression -> Inference m (Maybe MatchError)
   QueryMetavar :: Hole -> Inference m (Maybe Expression)
-  WeakNormalize :: Expression -> Inference m Expression
   RegisterIden :: Name -> Expression -> Inference m ()
 
 makeSem ''Inference
@@ -141,7 +140,6 @@ re ::
 re = reinterpret $ \case
   MatchTypes a b -> matchTypes' a b
   QueryMetavar h -> queryMetavar' h
-  WeakNormalize t -> weakNormalize' t
   RegisterIden i ty -> registerIden' i ty
   where
     registerIden' :: Members '[State InferenceState] r => Name -> Expression -> Sem r ()

tests/positive/TypeAlias.juvix

@@ -14,17 +14,20 @@ alias ≔ T;
 x : alias;
 x ≔ t;
 
-id : Type -> Type;
+id : Type → Type;
 id x ≔ x;
 
-flip : (Type -> Type -> Type) -> Type -> Type -> Type;
+flip : (Type → Type → Type) → id Type → Type → Type;
 flip f a b ≔ f b a;
 
 inductive Pair (A : Type) (B : Type) {
- mkPair : id T -> id (id A) -> B -> Pair A B;
+ mkPair : id T → id (id A) → B → Pair A B;
 };
 
-x' : flip Pair (id alias) T2;
+p : {A : Type} → A → Pair A A;
+p a ≔ mkPair t a a;
+
+x' : flip Pair (id _) T2;
 x' ≔ mkPair x t2 t;
 
 end;