Errors about ambiguous untouchable variable when using constraint variable in RankN type

The following code compiles and works:

{-# LANGUAGE
    ConstraintKinds
  , FlexibleInstances
  , MultiParamTypeClasses
  , GADTs
  , RankNTypes
  , ScopedTypeVariables
  , UndecidableSuperClasses
  #-}

import GHC.Types (Constraint)

main :: IO ()
main = do return ()

class (r a) => DynPS r a where
data PSAny r = forall a. DynPS r a => PSAny a

class Unconstrained a
instance Unconstrained a
instance DynPS Unconstrained ()

newtype DynLoad' r = DynLoad' {
  unDynLoad' :: forall ref. r ref => ref -> PSAny r
  }

loadAll
  :: forall a r . (DynPS r a)
  => DynLoad' r
  -> a -> Maybe a
loadAll loader r = undefined

testCallable :: IO (Maybe ())
testCallable = return $ loadAll (undefined :: DynLoad' Unconstrained) ()

However it's ugly having to expose DynLoad' in the API. Ideally we'd like to have:

loadAll2
  :: forall a r . (DynPS r a)
  => (forall ref. r ref => ref -> PSAny r)
  -> a -> Maybe a
loadAll2 loader r = loadAll (DynLoad' loader :: DynLoad' r) r

But this fails with:

Test3.hs:37:6: error:
    • Couldn't match type ‘r0’ with ‘r’
        ‘r0’ is untouchable
          inside the constraints: r0 ref
          bound by the type signature for:
                     loadAll2 :: forall ref. r0 ref => ref -> PSAny r0
          at Test3.hs:(37,6)-(39,17)
      ‘r’ is a rigid type variable bound by
        the type signature for:
          loadAll2 :: forall a (r :: * -> Constraint).
                      DynPS r a =>
                      (forall ref. r ref => ref -> PSAny r) -> a -> Maybe a
        at Test3.hs:(37,6)-(39,17)
      Expected type: ref -> PSAny r0
        Actual type: ref -> PSAny r
    • In the ambiguity check for ‘loadAll2’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        loadAll2 :: forall a r.
                    (DynPS r a) =>
                    (forall ref. r ref => ref -> PSAny r) -> a -> Maybe a
   |
37 |   :: forall a r . (DynPS r a)
   |      ^^^^^^^^^^^^^^^^^^^^^^^^...

It compiles if we enable AllowAmbiguousTypes, but are then forced to use TypeApplications as well to actually call it. :(

-- as above, but add:
{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}

-- and then:

testCallable2 :: IO (Maybe ())
--testCallable2 = return $ loadAll2 (undefined :: forall ref. Unconstrained ref => ref -> PSAny Unconstrained) ()
-- ^ doesn't work either
testCallable2 = return $ loadAll2 @() @Unconstrained undefined ()

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture