From ba06fd335b0541df179b05e648e6a82fb310a859 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Thu, 3 Oct 2019 17:15:25 -0700
Subject: [PATCH] test: add new elab issue from @joehendrix

---
 tests/elabissues/issues4.lean | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 tests/elabissues/issues4.lean

diff --git a/tests/elabissues/issues4.lean b/tests/elabissues/issues4.lean
new file mode 100644
index 0000000000..dc6b10370f
--- /dev/null
+++ b/tests/elabissues/issues4.lean
@@ -0,0 +1,23 @@
+-- From @joehendrix
+-- The imul doesn't type check as Lean won't try to coerce from a reg (bv 64) to a expr (bv ?u)
+
+inductive MCType
+| bv : Nat → MCType
+
+open MCType
+
+inductive Reg : MCType → Type
+| rax : Reg (bv 64)
+
+inductive Expr : MCType → Type
+| r : ∀{tp:MCType}, Reg tp → Expr tp
+| sextC {s:Nat} (x : Expr (bv s)) (t:Nat) : Expr (bv t)
+
+instance reg_is_expr {tp:MCType} : HasCoe (Reg tp) (Expr tp) := ⟨Expr.r⟩
+
+def bvmul {w:Nat} (x y : Expr (bv w)) : Expr (bv w) := x
+
+def sext {s:Nat} (x : Expr (bv s)) (t:Nat) : Expr (bv t) := Expr.sextC x t
+
+def imul {u:Nat} (e:Expr (bv 64)) : Expr (bv 128) :=
+  bvmul (sext Reg.rax 128) (sext e _)