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 |