ugly stub for checkCoerce

src/Agda/Core/Typechecker.agda

@@ -1,7 +1,7 @@
 {-# OPTIONS --allow-unsolved-metas #-}
 open import Haskell.Prelude
   hiding ( All; m; _,_,_)
-  renaming (_,_ to infixr 5 _,_)
+  renaming (_,_ to infixr 5 [_⨾_])
 
 open import Scope
 
@@ -32,9 +32,6 @@ open import Haskell.Extra.Erase
 private variable
   @0 α : Scope name
 
-postulate
-  convert   : (Γ : Context α) (@0 ty : Type α) (@0 a b : Term α) → Γ ⊢ a ≅ b ∶ ty
-
 reduceTo : (_ : Rezz _ α)
            (sig : Signature)
            (v : Term α)
@@ -129,18 +126,32 @@ checkCoerce : ∀ Γ (t : Term α)
             → (cty : Type α) -- the type we want to have
             → (tty : Type α) -- the type of types
             → TCM (Γ ⊢ t ∶ cty)
---FIXME: first reduce the type, patmatch on the type
---the depending on what the type is do either
---for vars
---for defs
---for cons
---for labmda
---for app
---for pi
---for sort
---the rest should be reduced away
-checkCoerce ctx t (s , d) cty tty = do
-  return $ TyConv d (convert ctx tty s cty)
+checkCoerce ctx t (gty , dgty) cty tty = do
+  --FIXME: first reduce the type, patmatch on the type
+  --the depending on what the type is do either
+  let r = rezzScope ctx
+  fuel      ← tcmFuel
+  rezz sig  ← tcmSignature
+
+  rgty ← reduceTo r sig gty fuel
+  rcty ← reduceTo r sig cty fuel
+  case [ rgty ⨾ rcty ] of λ where
+  --for vars
+    [ TVar x p ⟨ rpg ⟩ ⨾ TVar y q ⟨ rpc ⟩ ] → {!!}
+  --for defs
+    [ TDef x p ⟨ rpg ⟩ ⨾ TDef y q ⟨ rpc ⟩ ] → {!!}
+  --for cons
+    [ TCon c p lc ⟨ rpg  ⟩ ⨾ TCon d q ld ⟨ rpc ⟩ ] → {!!}
+  --for lambda
+    [ TLam x u ⟨ rpg ⟩ ⨾ TLam y v ⟨ rpc ⟩ ] → {!!}
+  --for app
+    [ TApp u e ⟨ rpg ⟩ ⨾ TApp v f ⟨ rpc ⟩ ] → {!!}
+  --for pi
+    [ TPi x su sv u v ⟨ rpg ⟩ ⨾ TPi y tu tv w z ⟨ rpc ⟩ ] → {!!}
+  --for sort
+    [ TSort s ⟨ rpg ⟩ ⨾ TSort t ⟨ rpc ⟩ ] → {!!}
+  --the rest should be reduced away
+    _ → tcError "sorry"
 
 checkType ctx t@(TVar x p) ty s = do
   tvar ← inferVar ctx x p