
But I feel there ought to be a way to apply this hack systematically, so that we can handle these cases, which are "easier" than full impredicativity. For example, as a dumb proposal, if we treated ($) and (.) as macros (inline before typechecking), that would give us correct typechecking for both these cases. So maybe some sort of stratification would solve our problem. Edward Excerpts from David Feuer's message of 2016-06-10 08:21:31 -0700:
I'm pretty sure we *could*, but special case hacks in the type checker are horrible. So we shouldn't. On Jun 10, 2016 11:13 AM, "Edward Z. Yang"
wrote: Excerpts from Brendan Hay's message of 2016-06-10 01:59:51 -0700:
* How does the use of ($) vs (.) fix this particular issue? (I'd naively assume the usage here would be equivalent.) I recall reading about ($)'s magical type alias somewhere - is this related?
When you say f $ a, where a is a polymorphic variable, we need to instantiate the type variables in ($) :: (a -> b) -> a -> b with quantified types; i.e., do an impredicative instantiation. GHC has never been able to do this, so there's a hack for the typechecker to treat 'f $ a' as if it were just 'f a' (no more impredicative instantiation).
(.) is not special cased similarly, which is why it doesn't work. I don't know if we could special case it to solve this problem.
Edward _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe