type applications and constraint kinds

Question

(I'm not entirely familiar with the inner workings of Haskell's constraint solver so this could likely be a rookie question.)

When trying to use type application on GHC 8.0.1, as shown in the following sample code

{-# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, ScopedTypeVariables, TypeApplications #-}
module Test where

import Data.Constraint

test0 :: forall (b :: *) . (forall a . a -> Bool) -> b -> Bool
test0 g = g @b

test1 :: forall (c :: * -> Constraint) (b :: *) . (c b) => (forall a . c a => a -> Bool) -> b -> Bool
test1 g = g @b

it gives me the following errors

• Could not deduce: c0 b
  from the context: c b
    bound by the type signature for:
               test1 :: c b => (forall a. c a => a -> Bool) -> b -> Bool
    at Test.hs:9:10-101
• In the ambiguity check for ‘test1’
  To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
  In the type signature:
    test1 :: forall (c :: * -> Constraint) (b :: *).
             (c b) => (forall a. c a => a -> Bool) -> b -> Bool

and

• Could not deduce: c a
  from the context: c b
    bound by the type signature for:
               test1 :: c b => (forall a. c a => a -> Bool) -> b -> Bool
    at Test.hs:9:10-101
  or from: c0 a
    bound by the type signature for:
               test1 :: c0 a => a -> Bool
    at Test.hs:9:10-101
• In the ambiguity check for ‘test1’
  To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
  In the type signature:
    test1 :: forall (c :: * -> Constraint) (b :: *).
             (c b) => (forall a. c a => a -> Bool) -> b -> Bool

test0 works where there is no constraint involved, but test1 doesn't.

Answer 1

If you have TypeApplications enabled, you should enable AllowAmbiguousTypes too. If you do so, the error goes away.

The ambiguity check rejects definitions t such that no t :: type annotation could ever typecheck. For example:

test1 :: Show a => Int
test1 = 0

If we try to use test1 elsewhere in our program, we find that there's no way to resolve the Show a constraint by way of :: annotation. Therefore the ambiguity check rejects the definition itself.

Of course, with type applications the ambiguity check becomes meaningless (arguably, it should be turned off by default in this case), since test1 @type is fine and completely determined whenever there is a Show type instance available.

Note that this is not the same as the famous show . read ambiguity. That still produces an error, with AllowAmbiguousTypes too:

test2 = show . read 
-- "ambiguous type variable prevents the constraint from being solved"

Operationally, values with c => t types are just functions from c-typed instances to t. Just defining test1 is fine, since we can always define a constant function. However, in show . read we need to supply instances as argument (or else there's no code to be run), and there's no way to resolve them. Using test1 without a type application would be similarly ambiguous.