[GHC] #15649: Errors about ambiguous untouchable variable when using constraint variable in RankN type

[GHC]

#15649: Errors about ambiguous untouchable variable when using constraint variable
in RankN type
-------------------------------------+-------------------------------------
           Reporter:  infinity0      |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following code compiles and works:

 {{{#!haskell
 {-# 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:

 {{{#!haskell
 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. :(

 {{{#!haskell
 -- 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 ()
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15649>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler