From f34b6948f7cf6c5cb9041d27eda5ab72946e7d18 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Tue, 29 Nov 2022 08:19:19 -0500
Subject: [PATCH] Work around ghc/ghc#22519 in what4 patch

We move around some uses of `coerce` to avoid coercing underneath `IO`, which
triggers ghc/ghc#22519 on HEAD.
---
 patches/what4-1.3.patch | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/patches/what4-1.3.patch b/patches/what4-1.3.patch
index 521cda5c..8dbb1193 100644
--- a/patches/what4-1.3.patch
+++ b/patches/what4-1.3.patch
@@ -28,6 +28,34 @@ index 6d91cda..8f247c3 100644
  
  -- | Record variables in a predicate that we are checking satisfiability of.
  recordAssertionVars :: Scope
+diff --git a/src/What4/Interface.hs b/src/What4/Interface.hs
+index edec041..c9af5ef 100644
+--- a/src/What4/Interface.hs
++++ b/src/What4/Interface.hs
+@@ -2589,8 +2589,9 @@ bvJoinVector :: forall sym n w. (1 <= w, IsExprBuilder sym)
+              -> NatRepr w
+              -> Vector.Vector n (SymBV sym w)
+              -> IO (SymBV sym (n * w))
+-bvJoinVector sym w =
+-  coerce $ Vector.joinWithM @IO @(SymBV' sym) @n bvConcat' w
++bvJoinVector sym w v = do
++  bv <- Vector.joinWithM @IO @(SymBV' sym) @n bvConcat' w $ coerce v
++  pure $ coerce bv
+   where bvConcat' :: forall l. (1 <= l)
+                   => NatRepr l
+                   -> SymBV' sym w
+@@ -2607,8 +2608,9 @@ bvSplitVector :: forall sym n w. (IsExprBuilder sym, 1 <= w, 1 <= n)
+               -> NatRepr w
+               -> SymBV sym (n * w)
+               -> IO (Vector.Vector n (SymBV sym w))
+-bvSplitVector sym n w x =
+-  coerce $ Vector.splitWithA @IO BigEndian bvSelect' n w (MkSymBV' @sym x)
++bvSplitVector sym n w x = do
++  bv <- Vector.splitWithA @IO BigEndian bvSelect' n w (MkSymBV' @sym x)
++  pure $ coerce bv
+   where
+     bvSelect' :: forall i. (i + w <= n * w)
+               => NatRepr (n * w)
 diff --git a/src/What4/Utils/AbstractDomains.hs b/src/What4/Utils/AbstractDomains.hs
 index 8b89aa5..77c8399 100644
 --- a/src/What4/Utils/AbstractDomains.hs
-- 
GitLab