title: agda-compute-normalised-maybe-toplevel shows the correct type, yet `refl` isn't accepted
body: <p>I'm trying to write a pretty print for a basic language syntax, with the property that the output of the pretty printer should correctly parse as the thing it's printing. I have the following:</p>
  
  <pre><code>data Syntax : Set where
    string : List Char -&gt; Syntax
  
  parse : List Char → Maybe Syntax
  parse ('"' ∷ '"' ∷ _) = just (string [])
  parse _ = nothing
  </code></pre>
  
  <p>The parser can only parse the string <code>""</code> as an empty literal string for now, but it's a start :)</p>
  
  <p>Next, I have my pretty printer:</p>
  
  <pre><code>pretty-lit : (s : Syntax) → pretty-printer-for (string l)
  pretty-lit (string []) = char '"' &lt;&gt; char '"', {!!}
  pretty-lit (string (x ∷ xs)) = {!!}
  </code></pre>
  
  <p>The pretty-printer-for type is:</p>
  
  <pre><code>pretty-printer-for : (s : Syntax) → Set
  pretty-printer-for s = Σ Doc (λ d → parse (display (render-pretty 80 d)) ≡ just s)
  </code></pre>
  
  <p>That is, a dependent product of a <code>Doc</code> (ala Wadler's pretty printing) and a proof that parsing the result of rendering that <code>Doc</code> to a string is indeed the syntax you started with.</p>
  
  <p>Now, the first hole in <code>pretty-lit</code> above has this goal:</p>
  
  <pre><code>Goal: parse
        (display (render-pretty 80 (cat (char '\"') (char '\"'))))
        ≡ just (string [])
  ————————————————————————————————————————————————————————————
  </code></pre>
  
  <p>If I completely comment out <code>pretty-lit</code> and use <code>agda-compute-normalised-maybe-toplevel</code>, then <code>parse (display (render-pretty 80 (cat (char '\"') (char '\"'))))</code> computes to <code>just (string [])</code>, which is what I'd expect. However, if I try and use <code>refl</code> as the contents of that hole, I get</p>
  
  <pre><code>parse
  (display (render-pretty (fromNat 80) (char '\"' &lt;&gt; char '\"')))
  != just (string []) of type Maybe Syntax
  when checking that the expression refl has type
  parse
  (display (render-pretty (fromNat 80) (char '\"' &lt;&gt; char '\"')))
  ≡ just (string [])
  </code></pre>
  
  <p>But I just checked and they are equal! Oddly, <code>pretty-lit</code> with holes (as above) is in scope, the <code>agda-computer-normalised-maybe-toplevel</code> <em>doesn't</em> compute <code>just (string [])</code>, but I have no idea why.</p>
  
  <p>Full source can be found at <a href="https://github.com/ocharles/agda-nixfmt/commit/4df637cce0621b3d9d8a3ee0a104f46523dcc908" rel="nofollow noreferrer">https://github.com/ocharles/agda-nixfmt/commit/4df637cce0621b3d9d8a3ee0a104f46523dcc908</a>, including the definition of my pretty printer.</p>