title: Erratic hole type resolution
body: <p>I recently found out that type holes combined with pattern matching on proofs provides a pretty nice Agda-like experience in Haskell. For example:</p>
  
  <pre><code>{-# LANGUAGE
      DataKinds, PolyKinds, TypeFamilies, 
      UndecidableInstances, GADTs, TypeOperators #-}
  
  data (==) :: k -&gt; k -&gt; * where
      Refl :: x == x
  
  sym :: a == b -&gt; b == a
  sym Refl = Refl 
  
  data Nat = Zero | Succ Nat
  
  data SNat :: Nat -&gt; * where
      SZero :: SNat Zero
      SSucc :: SNat n -&gt; SNat (Succ n)
  
  type family a + b where
      Zero   + b = b
      Succ a + b = Succ (a + b)
  
  addAssoc :: SNat a -&gt; SNat b -&gt; SNat c -&gt; (a + (b + c)) == ((a + b) + c)
  addAssoc SZero b c = Refl
  addAssoc (SSucc a) b c = case addAssoc a b c of Refl -&gt; Refl
  
  addComm :: SNat a -&gt; SNat b -&gt; (a + b) == (b + a)
  addComm SZero SZero = Refl
  addComm (SSucc a) SZero = case addComm a SZero of Refl -&gt; Refl
  addComm SZero (SSucc b) = case addComm SZero b of Refl -&gt; Refl
  addComm sa@(SSucc a) sb@(SSucc b) =
      case addComm a sb of
          Refl -&gt; case addComm b sa of
              Refl -&gt; case addComm a b of
                  Refl -&gt; Refl 
  </code></pre>
  
  <p>The really nice thing is that I can replace the right-hand sides of the <code>Refl -&gt; exp</code> constructions with a type hole, and my hole target types are updated with the proof, pretty much as with the <code>rewrite</code> form in Agda. </p>
  
  <p>However, sometimes the hole just fails to update:</p>
  
  <pre><code>(+.) :: SNat a -&gt; SNat b -&gt; SNat (a + b)
  SZero   +. b = b
  SSucc a +. b = SSucc (a +. b)
  infixl 5 +.
  
  type family a * b where
      Zero   * b = Zero
      Succ a * b = b + (a * b)
  
  (*.) :: SNat a -&gt; SNat b -&gt; SNat (a * b)
  SZero   *. b = SZero
  SSucc a *. b = b +. (a *. b)
  infixl 6 *.
  
  mulDistL :: SNat a -&gt; SNat b -&gt; SNat c -&gt; (a * (b + c)) == ((a * b) + (a * c))
  mulDistL SZero b c = Refl
  mulDistL (SSucc a) b c = 
      case sym $ addAssoc b (a *. b) (c +. a *. c) of
          -- At this point the target type is
          -- ((b + c) + (n * (b + c))) == (b + ((n * b) + (c + (n * c))))
          -- The next step would be to update the RHS of the equivalence:
          Refl -&gt; case addAssoc (a *. b) c (a *. c) of
              Refl -&gt; _ -- but the type of this hole remains unchanged...
  </code></pre>
  
  <p>Also, even though the target types do not necessarily line up inside the proof, if I paste in the whole thing from Agda it still checks fine:</p>
  
  <pre><code>mulDistL' :: SNat a -&gt; SNat b -&gt; SNat c -&gt; (a * (b + c)) == ((a * b) + (a * c))
  mulDistL' SZero b c = Refl
  mulDistL' (SSucc a) b c = case
      (sym $ addAssoc b (a *. b) (c +. a *. c),
      addAssoc (a *. b) c (a *. c),
      addComm (a *. b) c,
      sym $ addAssoc c (a *. b) (a *. c),
      addAssoc b c (a *. b +. a *. c),
      mulDistL' a b c
      ) of (Refl, Refl, Refl, Refl, Refl, Refl) -&gt; Refl
  </code></pre>
  
  <p>Do you have any ideas why this happens (or how I could do proof rewriting in a robust way)?</p>