Applying typed hole proposal leads to compilation failure

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

Applying typed hole proposal leads to compilation failure

Vlatko Basic

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'.

Why does GHC think those two are different and how to tell to GHC they are the same?


Best regards,

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 []




_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Applying typed hole proposal leads to compilation failure

mniip
> • 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

Emphasis on "rigid". It's not telling you to introduce a new type
variable and put that there. It's telling you that the type you need to
put there is an existing type variable's type.

When you write 'run :: MS c Int a -> (Either String a, Int)' you
implicitly mean 'run :: forall c.' which is exactly introducing a new
type variable.

> • 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)
This is the 'c' you bound with the implicit 'forall'. The compiler is
asked to verify that 'run' indeed works 'forall c1', so during
typechecking of the function body the 'c1' variable is also rigid.

>    ‘c’ is a rigid type variable bound by
>      the type signature for:
>        f1 :: forall (m :: * -> *) c. MonadIO m => c -> m Bool
This is the 'c' from the typed hole suggestion up above, still rigid.

A part of the typechecking algorithm is that two rigid type variables
cannot be equated.

The solution *actually* proposed by GHC in the wildcard suggestion is to
use the 'c' variable from 'f1's type for which you need to make it
scoped with an explicit 'forall':

        f1 :: forall c. (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)
            run = runMS c 0
            f2 :: MS c s Bool
            f2 = pure False
            f3 :: MS c s [Int]
            f3 = pure []
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Applying typed hole proposal leads to compilation failure

Brandon Allbery
Note that this also requires ScopedTypeVariables; the Haskell standard specifies that type variables are only in scope within the type signature, not the accompanying binding. Which is also why the explicit "forall" is required, to tell it to use the modified rules here, which otherwise could cause other code that expects standard Haskell behavior to fail to compile if it happens to reuse type variables from the signature.

On Fri, Aug 24, 2018 at 5:37 PM mniip <[hidden email]> wrote:
> • 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

Emphasis on "rigid". It's not telling you to introduce a new type
variable and put that there. It's telling you that the type you need to
put there is an existing type variable's type.

When you write 'run :: MS c Int a -> (Either String a, Int)' you
implicitly mean 'run :: forall c.' which is exactly introducing a new
type variable.

> • 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)
This is the 'c' you bound with the implicit 'forall'. The compiler is
asked to verify that 'run' indeed works 'forall c1', so during
typechecking of the function body the 'c1' variable is also rigid.

>    ‘c’ is a rigid type variable bound by
>      the type signature for:
>        f1 :: forall (m :: * -> *) c. MonadIO m => c -> m Bool
This is the 'c' from the typed hole suggestion up above, still rigid.

A part of the typechecking algorithm is that two rigid type variables
cannot be equated.

The solution *actually* proposed by GHC in the wildcard suggestion is to
use the 'c' variable from 'f1's type for which you need to make it
scoped with an explicit 'forall':

        f1 :: forall c. (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)
            run = runMS c 0
            f2 :: MS c s Bool
            f2 = pure False
            f3 :: MS c s [Int]
            f3 = pure []
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


--
brandon s allbery kf8nh

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Applying typed hole proposal leads to compilation failure

mniip
On Fri, Aug 24, 2018 at 06:25:34PM -0400, Brandon Allbery wrote:
> Note that this also requires ScopedTypeVariables; the Haskell standard
> specifies that type variables are only in scope within the type signature,
> not the accompanying binding. Which is also why the explicit "forall" is
> required, to tell it to use the modified rules here, which otherwise could
> cause other code that expects standard Haskell behavior to fail to compile
> if it happens to reuse type variables from the signature.

I had thought of mentioning this but their original snippet included the
extension so I thought they already knew.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Applying typed hole proposal leads to compilation failure

Vlatko Basic
In reply to this post by mniip

Hi mniip,

Let me first apologise for my very late response. I went for a visit to the analog world, and stayed much longer than planned. :-)


I have ScopedTypeVariables enabled as a default extension in .cabal file, but have never encountered such an error, to have to manually specify forall just for making scoped types to work.

I'm using local signatures quite often, but still not quite clear as to how/where the original code differs, for example, from this one (which compiles fine):


mkTransUnitValTag :: (HasGlobals s) => InNode -> MS c s TransUnitValT
mkTransUnitValTag e@(Element "tuv" as (cleanBlank -> cs) _) = do
  TransUnitValT <$> attrGlobDef e glbDataType "datatype"   as -- tuvDataType

                 ...
                <*> parseTag    e "seg" mkSegTag           cs -- tuvSeg
  where
    mkSegTag :: InNode -> MS c s Content
    mkSegTag (Element "seg" _as ss _) = checkContent =<< mapM mkContentTag ss


Is the main diff that 'run' is having monad stack as input and is running it, while 'mkSegTag' is run in it (so forall does not have to be specified manually)?

    mkSegTag :: InNode -> MS c s Content

    f1 :: forall m c. (MonadIO m) => c -> m ()  -- original code

       where run :: MS c Int a -> (Either String a, Int)


Thanks for pointing me to read the whole error/warning. Everything is actually written there, but seems I have developed some kind of forall blindness. :-(



On 24/08/2018 23:36, mniip wrote:
• 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
Emphasis on "rigid". It's not telling you to introduce a new type
variable and put that there. It's telling you that the type you need to
put there is an existing type variable's type.

When you write 'run :: MS c Int a -> (Either String a, Int)' you
implicitly mean 'run :: forall c.' which is exactly introducing a new
type variable.

• 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)
This is the 'c' you bound with the implicit 'forall'. The compiler is
asked to verify that 'run' indeed works 'forall c1', so during
typechecking of the function body the 'c1' variable is also rigid.

   ‘c’ is a rigid type variable bound by
     the type signature for:
       f1 :: forall (m :: * -> *) c. MonadIO m => c -> m Bool
This is the 'c' from the typed hole suggestion up above, still rigid.

A part of the typechecking algorithm is that two rigid type variables
cannot be equated.

The solution *actually* proposed by GHC in the wildcard suggestion is to
use the 'c' variable from 'f1's type for which you need to make it
scoped with an explicit 'forall':

	f1 :: forall c. (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)
	    run = runMS c 0
	    f2 :: MS c s Bool
	    f2 = pure False
	    f3 :: MS c s [Int]
	    f3 = pure []
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.