title: Is Idris really "strictly evaluated?"
body: <p>Coming from Haskell, I was reading about Idris' story regarding laziness (non-strictness). I trolled the recent release notes, and <a href="http://www.idris-lang.org/idris-0-9-12-released/">found code</a> akin to the following</p>
  
  <pre><code>myIf : (b : Bool) -&gt; (t : Lazy a) -&gt; (e : Lazy a) -&gt; a
  myIf True t e = t
  myIf False t e = e
  </code></pre>
  
  <p>I wrote a simple factorial function to test it</p>
  
  <pre><code>myFact : Int -&gt; Int
  myFact n = myIf (n == 1) 1 (n * myFact (n-1))
  </code></pre>
  
  <p>I ran it and it worked!</p>
  
  <pre><code>&gt; myFact 5
  120 : Int
  </code></pre>
  
  <p>I decided to break it by changing the type signature of <code>myIf</code> to</p>
  
  <pre><code>myIf : (b : Bool) -&gt; a -&gt; a -&gt; a
  </code></pre>
  
  <p>I reloaded the <code>idris</code> repl, and ran <code>myFact 5</code> again expecting an infinite recursion. To my surprise, it still worked the same way!</p>
  
  <p>Can idris figure out when it should avoid strictness? Why didn't this recurse forever?</p>
  
  <p>I'm using Idris 0.9.15 and none of the release notes between now and the linked notes, mention any changes.</p>