[Haskell-cafe] Generalization of types during inference

[Jake McArthur]

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:

infer :: Term -> Type
check :: Term -> Type -> Bool

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`.

On Sun, Jun 7, 2020 at 4:19 PM Olaf Klinke <olf at aatal-apotheke.de> wrote:

> > f 0 x = 0
> > f 1 x = f 0 ()
> > f n x = f (n-1) 'a'
>
> That's very interesting, I learned something new about GHC today. I
> used to believe that my Haskell compiler always type checks
> declarations on its own, and after that unifies its result with the
> type declaration that I provide. Polymorphic recursion yields a case
> where the compiler's inference procedure is evidently not independent
> of my provided type declaration. Can the above be abused to compile
> programs containing false type declarations? (It seems the answer is
> no, but maybe I lack the fantasy.)
>
> Thanks,
> Olaf
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200607/94ea7cca/attachment.html>