@@ 79,8 79,8 @@
<p><strong>decidable</strong>, since type inference is only used for variable initialization</p>
<h3 id="haskell">Haskell</h3>
<p>1998 standard, no extensions: <strong>decidable</strong>, variant of HM</p>
-<p>2010 standard, no extensions: <strong>decidable</strong>, restriction of System F</p>
-<p>with sufficient<a href="#fn1" class="footnote-ref" id="fnref1"><sup>1</sup></a> extensions: <strong>undecidable</strong>, as type checking in System F is undecidable. There exist <a href="https://www.lochan.org/keith/publications/undec.html">Turing Machines in Haskell types</a>. A simpler variant is to implement the <a href="https://mail.haskell.org/pipermail/haskell/2006-August/018355.html">SKI calculus</a>.</p>
+<p>2010 standard, no extensions: <strong>decidable</strong>, restriction of <a href="https://wikipedia.org/wiki/System_F">System F</a></p>
+<p>with sufficient<a href="#fn1" class="footnote-ref" id="fnref1"><sup>1</sup></a> extensions: <strong>undecidable</strong>, as there exist <a href="https://www.lochan.org/keith/publications/undec.html">Turing Machines in Haskell types</a>. A simpler variant is to implement the <a href="https://mail.haskell.org/pipermail/haskell/2006-August/018355.html">SKI calculus</a>.</p>
<h3 id="idris">Idris</h3>
<p><strong>decidable</strong>, surprisingly. Idris has dependent types, but <a href="https://docs.idris-lang.org/en/latest/faq/faq.html#evaluation-at-the-repl-doesn-t-behave-as-i-expect-what-s-going-on">at compile time it will only evaluate expressions which it knows to be total (terminating and covering all inputs)</a>.</p>
<h3 id="java">Java</h3>