constraint, function composition, and let abstraction in Haskell

Question

Is there a simple explanation as to why ko1 and ko2 fail ?

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module SOQuestionExistential where

import Data.Proxy

------------------------------------------------------------------------------

class C s where
  important_stuff :: proxy s -> a

compute_ok :: forall r. (forall s. C s => Proxy s -> IO r) -> IO r
compute_ok k = undefined

unref_ok :: Proxy s -> Proxy s -> IO ()
unref_ok _ _ = return ()

----

ok :: (forall s. C s => t -> Proxy s) -> t -> IO ()
ok calc t = compute_ok (unref_ok (calc t))

ko1 :: (forall s. C s => t -> Proxy s) -> t -> IO ()
ko1 calc t = (compute_ok . unref_ok) (calc t)

-- • Couldn't match type ‘s’ with ‘s0’
--   ‘s’ is a rigid type variable bound by
--     a type expected by the context:
--       forall s. C s => Proxy s -> IO ()

ok' :: (forall s. C s => t -> Proxy s) -> t -> IO ()
ok' calc t = compute_ok (unref_ok (let proxy_secret_s = calc t in proxy_secret_s))

ko2 :: (forall s. C s => t -> Proxy s) -> t -> IO ()
ko2 calc t = let proxy_secret_s = calc t in compute_ok (unref_ok (proxy_secret_s))


-- • No instance for (C s1) arising from a use of ‘calc’
-- • In the expression: calc t
--   In an equation for ‘proxy_secret_s’: proxy_secret_s = calc t
--   In the expression:
--     let proxy_secret_s = calc t
--     in compute_ok (unref_ok (proxy_secret_s))typec

edit : added the error message

Answer 1

Haskell's type system is predicative, meaning that when we use a polymorphic value foo :: forall a . ... the type system can only instantiate a with monomorphic (forall-free) types.

So, why is there a difference between these lines?

compute_ok (unref_ok ...)
(compute_ok . unref_ok) ...

In the first one, the type checker is able to check (unref_ok ...), generalize its result to the needed type (forall s. C s => Proxy s -> IO r), and pass that to compute_ok.

In the second case, however, compute_ok is not applied to an argument, but rather it is passed as an argument to function (.). The code really means

(.) compute_ok unref_ok ...

Now, what is the type of function (.)?

(.) :: (b->c) -> (a->b) -> (a->c)

To make (compute_ok . unref_ok) work we would need to choose b ~ (forall s. C s => Proxy s -> IO r) but, alas, this is a polymorphic type and predicativity forbids this choice for b.

Several attempts at making Haskell "less predicative" and allow certain kinds of impredicativity have been proposed by the GHC devs. One of them has even been implemented as an extension, and then de-facto deprecated since it does not work that well with the several other extensions. So, in fact, Haskell at this time does not allow impredicativity. This might change in the future.

A few final notes:

• While we can not instantiate b ~ forall ..., we can instantiate b ~ T where newtype T = T (forall ...) since this is handled just fine by the type system. Of course, using that requires wrapping/unwrapping which is not that convenient, but in principle it is an option.

• The predicativity problem, in principle, also applies to the ($) :: (a->b)->a->b operator. In this specific case, though, the GHC devs decided to patch the type system with an ad-hoc solution: f $ x is type checked as f x, allowing f to take a polymorphic input. This special case does not extend to .: f . g . h $ x is not type checked as f (g (h x)) which would save the day in the posted code.

---

The second example can be fixed by giving an explicit polymorphic signature to proxy_secret_s.

ko2 :: (forall s. C s => t -> Proxy s) -> t -> IO ()
ko2 calc t = let 
   proxy_secret_s :: forall s. C s => Proxy s
   proxy_secret_s = calc t 
   in compute_ok (unref_ok (proxy_secret_s))

or, alternatively, disabling the Dreaded Monomorphism Restriction:

{-# LANGUAGE NoMonomorphismRestriction #-}

I won't repeat the excellent explanation of the DMR which can be found in this answer. To make it very brief, Haskell tries hard to assign a monomorphic type to non functions like proxy_secret_s since in some cases that could cause to the same value to be recomputed multiple times. E.g. let x = expensiveFunction y z in x + x could evaluate the expensive function twice if x has a polymorphic type.