add eq-type

src/Kernel/Clarify/Clarify.hs

@@ -727,6 +727,8 @@ clarifyMagic h tenv der = do
               C.Primitive (C.Magic (LM.CallType funcVar arg1Var arg2Var))
     M.InspectType {} ->
       error "InspectType should be evaluated during inline expansion"
+    M.EqType {} ->
+      error "EqType should be evaluated during inline expansion"
     M.ShowType _ _ ->
       error "ShowType should be evaluated during inline expansion"
     M.TextCons _ _ _ ->

src/Kernel/Elaborate/Elaborate.hs

@@ -425,6 +425,10 @@ elaborate' h term = do
           typeValueExpr' <- elaborateType h typeValueExpr
           typeExpr' <- elaborateType h typeExpr
           return $ m :< TM.Magic (M.InspectType mid typeValueExpr' typeExpr')
+        M.EqType moduleID typeExpr1 typeExpr2 -> do
+          typeExpr1' <- elaborateType h typeExpr1
+          typeExpr2' <- elaborateType h typeExpr2
+          return $ m :< TM.Magic (M.EqType moduleID typeExpr1' typeExpr2')
         M.ShowType textTypeExpr typeExpr -> do
           textTypeExpr' <- elaborateType h textTypeExpr
           typeExpr' <- elaborateType h typeExpr

src/Kernel/Elaborate/Internal/EnsureAffinity.hs

@@ -237,6 +237,10 @@ analyze h term = do
           cs1 <- analyzeType h typeValueExpr
           cs2 <- analyzeType h typeExpr
           return $ cs1 ++ cs2
+        M.EqType _ typeExpr1 typeExpr2 -> do
+          cs1 <- analyzeType h typeExpr1
+          cs2 <- analyzeType h typeExpr2
+          return $ cs1 ++ cs2
         M.ShowType textTypeExpr typeExpr -> do
           cs1 <- analyzeType h textTypeExpr
           cs2 <- analyzeType h typeExpr

src/Kernel/Elaborate/Internal/Infer.hs

@@ -401,6 +401,14 @@ infer h term =
           typeValueExpr' <- inferType h typeValueExpr
           typeExpr' <- inferType h typeExpr
           return (m :< WT.Magic (M.WeakMagic $ M.InspectType mid typeValueExpr' typeExpr'), typeValueExpr')
+        M.EqType moduleID typeExpr1 typeExpr2 -> do
+          typeExpr1' <- inferType h typeExpr1
+          typeExpr2' <- inferType h typeExpr2
+          let boolSGL = SGL.StrictGlobalLocator {moduleID, sourceLocator = SL.boolLocator}
+          let boolTypeDD = DD.newByGlobalLocator boolSGL BN.boolType
+          let boolTypeVar = m :< WT.TVarGlobal (AttrVG.Attr {argNum = AN.zero, isConstLike = True}) boolTypeDD
+          let boolType = m :< WT.TyApp boolTypeVar []
+          return (m :< WT.Magic (M.WeakMagic $ M.EqType moduleID typeExpr1' typeExpr2'), boolType)
         M.ShowType textTypeExpr typeExpr -> do
           textTypeExpr' <- inferType h textTypeExpr
           typeExpr' <- inferType h typeExpr

src/Kernel/Parse/Internal/Discern.hs

@@ -798,6 +798,12 @@ discernMagic h m magic =
       typeValueExpr <- discernType h typeValueVar
       typeExpr' <- discernType h typeExpr
       return $ M.WeakMagic $ M.InspectType coreModuleID typeValueExpr typeExpr'
+    RT.EqType (_, (typeExpr1, _)) (_, (typeExpr2, _)) -> do
+      ensureCompileStage m h "inline magic (`eq-type`)"
+      coreModuleID <- Alias.resolveModuleAlias (H.aliasHandle h) m coreModuleAlias
+      typeExpr1' <- discernType h typeExpr1
+      typeExpr2' <- discernType h typeExpr2
+      return $ M.WeakMagic $ M.EqType coreModuleID typeExpr1' typeExpr2'
     RT.ShowType _ (_, (typeExpr, _)) -> do
       textType <- liftEither (locatorToTypeVar m coreText) >>= discernType h
       typeExpr' <- discernType h typeExpr

src/Kernel/Parse/Internal/RawTerm.hs

@@ -638,6 +638,7 @@ rawTermMagic h m c = do
       rawTermMagicGlobal h m c,
       rawTermMagicCallType h m c,
       rawTermMagicInspectType h m c,
+      rawTermMagicEqType h m c,
       rawTermMagicShowType h m c,
       rawTermMagicTextCons h m c,
       rawTermMagicTextUncons h m c,
@@ -743,6 +744,14 @@ rawTermMagicInspectType h m c = do
     typeExpr <- rawType h
     return $ \_ c2 -> m :< RT.Magic c (RT.InspectType (c2, typeExpr))
 
+rawTermMagicEqType :: Handle -> Hint -> C -> Parser (RT.RawTerm, C)
+rawTermMagicEqType h m c = do
+  rawTermMagicBase "eq-type" $ do
+    typeExpr1 <- rawType h
+    c3 <- delimiter ","
+    typeExpr2 <- rawType h
+    return $ \_ c2 -> m :< RT.Magic c (RT.EqType (c2, typeExpr1) (c3, typeExpr2))
+
 rawTermMagicShowType :: Handle -> Hint -> C -> Parser (RT.RawTerm, C)
 rawTermMagicShowType h m c = do
   rawTermMagicBase "show-type" $ do

src/Language/Common/Magic.hs

@@ -12,6 +12,7 @@ import Language.Common.ModuleID qualified as MID
 data Magic lt ty a
   = LowMagic (LM.LowMagic lt ty a)
   | InspectType MID.ModuleID ty ty -- typeValueExpr, e (both types)
+  | EqType MID.ModuleID ty ty
   | ShowType ty ty
   | TextCons ty a a
   | TextUncons MID.ModuleID a
@@ -27,6 +28,8 @@ instance Functor (Magic lt ty) where
         LowMagic (fmap f magic)
       InspectType mid typeValueExpr e ->
         InspectType mid typeValueExpr e
+      EqType mid t1 t2 ->
+        EqType mid t1 t2
       ShowType textTypeExpr typeExpr ->
         ShowType textTypeExpr typeExpr
       TextCons textTypeExpr rune text ->
@@ -43,6 +46,8 @@ instance Foldable (Magic lt ty) where
         foldMap f magic
       InspectType {} ->
         mempty
+      EqType {} ->
+        mempty
       ShowType {} ->
         mempty
       TextCons _ rune text ->
@@ -59,6 +64,8 @@ instance Traversable (Magic lt ty) where
         LowMagic <$> traverse f magic
       InspectType mid typeValueExpr e ->
         pure $ InspectType mid typeValueExpr e
+      EqType mid t1 t2 ->
+        pure $ EqType mid t1 t2
       ShowType textTypeExpr typeExpr ->
         pure $ ShowType textTypeExpr typeExpr
       TextCons textTypeExpr rune text ->

src/Language/RawTerm/RawTerm.hs

@@ -307,6 +307,7 @@ data RawMagic
   | OpaqueValue C (EL RawTerm)
   | CallType C (EL RawTerm) (EL RawTerm) (EL RawTerm)
   | InspectType (EL RawType)
+  | EqType (EL RawType) (EL RawType)
   | ShowType C (EL RawType)
   | TextCons C (EL RawTerm) (EL RawTerm)
   | TextUncons C (EL RawTerm)

src/Language/RawTerm/RawTerm/ToDoc.hs

@@ -335,6 +335,17 @@ toDoc term =
             [ attachComment c $ D.text "magic inspect-type",
               SE.decode $ SE.fromListWithComment (Just SE.Paren) SE.Comma [(c1, (typeToDoc e, c2))]
             ]
+        EqType (c1, (t1, c2)) (c3, (t2, c4)) -> do
+          D.join
+            [ attachComment c $ D.text "magic eq-type",
+              SE.decode $
+                SE.fromListWithComment
+                  (Just SE.Paren)
+                  SE.Comma
+                  [ (c1, (typeToDoc t1, c2)),
+                    (c3, (typeToDoc t2, c4))
+                  ]
+            ]
         ShowType c1 (c2, (typeExpr, c3)) -> do
           D.join
             [ attachComment (c ++ c1) $ D.text "magic show-type",

src/Language/Term/FreeVars.hs

@@ -157,6 +157,8 @@ freeVarsMagic magic =
       freeVarsLowMagic lowMagic
     M.InspectType _ typeValueExpr e ->
       S.union (freeVarsType typeValueExpr) (freeVarsType e)
+    M.EqType _ typeExpr1 typeExpr2 ->
+      S.union (freeVarsType typeExpr1) (freeVarsType typeExpr2)
     M.ShowType textTypeExpr typeExpr ->
       S.union (freeVarsType textTypeExpr) (freeVarsType typeExpr)
     M.TextCons textTypeExpr rune text ->

src/Language/Term/FreeVarsWithHints.hs

@@ -158,6 +158,8 @@ freeVarsWithHintsMagic magic =
       freeVarsWithHintsLowMagic lowMagic
     M.InspectType _ typeValueExpr e ->
       S.union (freeVarsWithHintsType typeValueExpr) (freeVarsWithHintsType e)
+    M.EqType _ typeExpr1 typeExpr2 ->
+      S.union (freeVarsWithHintsType typeExpr1) (freeVarsWithHintsType typeExpr2)
     M.ShowType textTypeExpr typeExpr ->
       S.union (freeVarsWithHintsType textTypeExpr) (freeVarsWithHintsType typeExpr)
     M.TextCons textTypeExpr rune text ->

src/Language/Term/Inline.hs

@@ -309,6 +309,10 @@ inline' h term = do
         M.InspectType mid _ typeExpr -> do
           typeExpr' <- inlineType' h typeExpr
           Magic.evaluateInspectType h m mid typeExpr' >>= inline' h
+        M.EqType moduleID typeExpr1 typeExpr2 -> do
+          typeExpr1' <- inlineType' h typeExpr1
+          typeExpr2' <- inlineType' h typeExpr2
+          Magic.evaluateEqType m moduleID typeExpr1' typeExpr2'
         M.ShowType textTypeExpr typeExpr -> do
           textTypeExpr' <- inlineType' h textTypeExpr
           typeExpr' <- inlineType' h typeExpr

src/Language/Term/Inline/Magic.hs

@@ -1,5 +1,6 @@
 module Language.Term.Inline.Magic
   ( evaluateInspectType,
+    evaluateEqType,
     evaluateShowType,
     evaluateTextCons,
     evaluateTextUncons,
@@ -28,13 +29,14 @@ import Language.Common.CreateSymbol qualified as Gensym
 import Language.Common.DefiniteDescription qualified as DD
 import Language.Common.Discriminant qualified as D
 import Language.Common.Ident.Reify qualified as Ident
-import Language.Common.VarKind qualified as VK
 import Language.Common.IsConstLike (IsConstLike)
 import Language.Common.ModuleID qualified as MID
 import Language.Common.PrimType qualified as PT
 import Language.Common.Rune qualified as Rune
 import Language.Common.SourceLocator qualified as SL
 import Language.Common.StrictGlobalLocator qualified as SGL
+import Language.Common.VarKind qualified as VK
+import Language.Term.Eq qualified as TermEq
 import Language.Term.Inline.Handle
 import Language.Term.PrimValue qualified as PV
 import Language.Term.Term qualified as TM
@@ -100,6 +102,11 @@ evaluateInspectType h m moduleID typeExpr = do
         "inspect-type: unable to determine type value for this type expression. Got: "
           <> toTextType (weakenType typeExpr)
 
+evaluateEqType :: Hint -> MID.ModuleID -> TM.Type -> TM.Type -> App TM.Term
+evaluateEqType m moduleID typeExpr1 typeExpr2 = do
+  let isEqual = TermEq.eqType typeExpr1 typeExpr2
+  return $ constructBoolTerm m moduleID isEqual
+
 makeVectorDD :: MID.ModuleID -> DD.DefiniteDescription
 makeVectorDD moduleID = do
   let vectorSGL = SGL.StrictGlobalLocator {moduleID, sourceLocator = SL.vectorLocator}
@@ -325,7 +332,7 @@ constructBoolTerm hint moduleID value = do
   let boolTypeDD = DD.newByGlobalLocator boolSgl BN.boolType
   let trueDD = DD.newByGlobalLocator boolSgl BN.trueConstructor
   let falseDD = DD.newByGlobalLocator boolSgl BN.falseConstructor
-  let consNameList = [(trueDD, [], True), (falseDD, [], True)]
+  let consNameList = [(falseDD, [], True), (trueDD, [], True)]
   let (consName, discriminant) =
         if value
           then (trueDD, D.increment D.zero)

src/Language/Term/Refresh.hs

@@ -118,6 +118,10 @@ refreshMagic h magic =
       typeValueExpr' <- refreshType h typeValueExpr
       typeExpr' <- refreshType h typeExpr
       return $ M.InspectType mid typeValueExpr' typeExpr'
+    M.EqType moduleID typeExpr1 typeExpr2 -> do
+      typeExpr1' <- refreshType h typeExpr1
+      typeExpr2' <- refreshType h typeExpr2
+      return $ M.EqType moduleID typeExpr1' typeExpr2'
     M.ShowType textTypeExpr typeExpr -> do
       textTypeExpr' <- refreshType h textTypeExpr
       typeExpr' <- refreshType h typeExpr

src/Language/Term/Subst.hs

@@ -409,6 +409,10 @@ substMagic h sub magic =
       typeValueExpr' <- substType h sub typeValueExpr
       e' <- substType h sub e
       return $ M.InspectType mid typeValueExpr' e'
+    M.EqType moduleID typeExpr1 typeExpr2 -> do
+      typeExpr1' <- substType h sub typeExpr1
+      typeExpr2' <- substType h sub typeExpr2
+      return $ M.EqType moduleID typeExpr1' typeExpr2'
     M.ShowType textTypeExpr typeExpr -> do
       textTypeExpr' <- substType h sub textTypeExpr
       typeExpr' <- substType h sub typeExpr

src/Language/Term/Weaken.hs

@@ -16,7 +16,6 @@ import Language.Common.Binder
 import Language.Common.DecisionTree qualified as DT
 import Language.Common.DefaultArgs qualified as DefaultArgs
 import Language.Common.Foreign qualified as F
-import Language.Common.Ident
 import Language.Common.ImpArgs qualified as ImpArgs
 import Language.Common.LamKind qualified as LK
 import Language.Common.LowMagic qualified as LM
@@ -172,6 +171,8 @@ weakenMagic m magic = do
               LM.CallType (weaken func) (weaken arg1) (weaken arg2)
     M.InspectType mid typeValueExpr e ->
       M.WeakMagic $ M.InspectType mid (weakenType typeValueExpr) (weakenType e)
+    M.EqType moduleID typeExpr1 typeExpr2 ->
+      M.WeakMagic $ M.EqType moduleID (weakenType typeExpr1) (weakenType typeExpr2)
     M.ShowType textTypeExpr typeExpr ->
       M.WeakMagic $ M.ShowType (weakenType textTypeExpr) (weakenType typeExpr)
     M.TextCons textTypeExpr rune text ->

src/Language/WeakTerm/FreeVars.hs

@@ -112,6 +112,8 @@ freeVarsMagicTerm (M.WeakMagic magic) =
       freeVarsLowMagicTerm lowMagic
     M.InspectType {} ->
       S.empty
+    M.EqType {} ->
+      S.empty
     M.ShowType {} ->
       S.empty
     M.TextCons _ rune text ->
@@ -280,6 +282,8 @@ freeVarsMagic (M.WeakMagic magic) =
       freeVarsLowMagic lowMagic
     M.InspectType _ typeValueExpr e ->
       S.union (freeVarsType typeValueExpr) (freeVarsType e)
+    M.EqType _ typeExpr1 typeExpr2 ->
+      S.union (freeVarsType typeExpr1) (freeVarsType typeExpr2)
     M.ShowType textTypeExpr typeExpr ->
       S.union (freeVarsType textTypeExpr) (freeVarsType typeExpr)
     M.TextCons textTypeExpr rune text ->

src/Language/WeakTerm/Subst.hs

@@ -445,6 +445,10 @@ substMagic h sub (WT.WeakMagic magic) = do
       typeValueExpr' <- substType h sub typeValueExpr
       e' <- substType h sub e
       return $ M.InspectType sgl typeValueExpr' e'
+    M.EqType moduleID typeExpr1 typeExpr2 -> do
+      typeExpr1' <- substType h sub typeExpr1
+      typeExpr2' <- substType h sub typeExpr2
+      return $ M.EqType moduleID typeExpr1' typeExpr2'
     M.ShowType textTypeExpr typeExpr -> do
       textTypeExpr' <- substType h sub textTypeExpr
       typeExpr' <- substType h sub typeExpr

src/Language/WeakTerm/ToText.hs

@@ -364,6 +364,8 @@ showMagic (M.WeakMagic magic) =
       showLowMagic lowMagic
     M.InspectType _ typeValueExpr e ->
       "magic inspect-type" <> inParen (toTextType typeValueExpr <> ", " <> toTextType e)
+    M.EqType _ typeExpr1 typeExpr2 ->
+      "magic eq-type" <> inParen (toTextType typeExpr1 <> ", " <> toTextType typeExpr2)
     M.ShowType textTypeExpr typeExpr ->
       "magic show-type" <> inParen (toTextType textTypeExpr <> ", " <> toTextType typeExpr)
     M.TextCons textTypeExpr rune text ->