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