Hello Cafe,

I encountered a strange issue regarding typed hole. If I ask GHC (8.4.3) for a typed hole proposal, it says 'use c', but if I use 'c', it complains that it can't unify 'c' and 'c1'.

vlatko

Typed hole proposal:
  • Found type wildcard ‘_c’ standing for ‘c’
   Where: ‘c’ is a rigid type variable bound by
            the type signature for:
              f1 :: forall (m :: * -> *) c. MonadIO m => c -> m Bool
            at Test.hs:15:1-32
  • In the type signature:
     run :: MS _c Int a -> (Either String a, Int)

Error when typed hole used:
  • Couldn't match type ‘c1’ with ‘c’
   ‘c1’ is a rigid type variable bound by
     the type signature for:
       run :: forall c1 a. MS c1 Int a -> (Either String a, Int)
     at Test.hs:21:5-47
   ‘c’ is a rigid type variable bound by
     the type signature for:
       f1 :: forall (m :: * -> *) c. MonadIO m => c -> m Bool
     at Test.hs:15:1-32
   Expected type: MS c1 Int a -> (Either String a, Int)
     Actual type: MS c Int a -> (Either String a, Int)

Minimal runnable example:

{-# LANGUAGE ScopedTypeVariables, PartialTypeSignatures #-}
module Test where

import Prelude
import Control.Monad.IO.Class     (MonadIO)
import Control.Monad.Trans.Except (ExceptT, runExceptT)
import Control.Monad.Trans.Reader (Reader,  runReader)
import Control.Monad.Trans.State  (StateT,  runStateT)

type MS c s = ExceptT String (StateT s (Reader c))

runMS :: c -> s -> MS c s a -> (Either String a, s)
runMS c s f = runReader (runStateT (runExceptT f) s) c

f1 :: (MonadIO m) => c -> m ()
f1 c = do
  let _x1 = run f2
  let _x2 = run f3
  return ()
  where
    run :: MS _c Int a -> (Either String a, Int)  --- failure or success, 'c' or '_'
    run = runMS c 0
    f2 :: MS c s Bool
    f2 = pure False
    f3 :: MS c s [Int]
    f3 = pure []