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 
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information