<div dir="ltr">I don't actually know much about GHC's type checker itself, but I think it uses a form of bidirectional type checking. A bidirectional type checker has two modes:<div><br></div><div>infer :: Term -> Type</div><div>check :: Term -> Type -> Bool</div><div><br></div><div>The syntax is divided into two classes. The types for one of these classes can be inferred, but the other can only be checked. Given a type checkable term, you can create a type inferable term by giving it a type annotation. That is, `infer (x :: T) = check x T`.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Jun 7, 2020 at 4:19 PM Olaf Klinke <<a href="mailto:olf@aatal-apotheke.de">olf@aatal-apotheke.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">> f 0 x = 0<br>
> f 1 x = f 0 ()<br>
> f n x = f (n-1) 'a'<br>
<br>
That's very interesting, I learned something new about GHC today. I<br>
used to believe that my Haskell compiler always type checks<br>
declarations on its own, and after that unifies its result with the<br>
type declaration that I provide. Polymorphic recursion yields a case<br>
where the compiler's inference procedure is evidently not independent<br>
of my provided type declaration. Can the above be abused to compile<br>
programs containing false type declarations? (It seems the answer is<br>
no, but maybe I lack the fantasy.)<br>
<br>
Thanks,<br>
Olaf<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>