CODEWITHSUNDEEP
haskelltypes
zarazek
zarazek

Reputation: 51

Correct behaviour when in GHCI, type error when in file

Given the definition:

 {-# LANGUAGE ExistentialQuantification, TypeFamilies, FlexibleInstances, FlexibleContexts, ScopedTypeVariables #-}
 class Monad m => RunableMonad m where
   type ReturnType m :: * -> *
   run :: m a -> ReturnType m a

when I type in GHCI

:t \x -> [run $ return x]

it gives me correct type of expression:

\x -> [run $ return x] :: RunableMonad m => a -> [ReturnType m a]

but when I put definition the following definition into the file, it gives me a type error:

single :: RunableMonad m => a -> [ReturnType m a]
single x = [run $ return x]

Could not deduce (ReturnType m0 ~ ReturnType m)
from the context (RunableMonad m)
  bound by the type signature for
             single :: RunableMonad m => a -> [ReturnType m a]
  at concurrency-simulator.hs:467:11-49
NB: ‘ReturnType’ is a type function, and may not be injective
The type variable ‘m0’ is ambiguous
Expected type: a -> [ReturnType m a]
  Actual type: a -> [ReturnType m0 a]
In the ambiguity check for:
  forall a (m :: * -> *). RunableMonad m => a -> [ReturnType m a]
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature for ‘single’:
  single :: RunableMonad m => a -> [ReturnType m a]

Upvotes: 2

Views: 79

Answers (3)

user2407038
user2407038

Reputation: 14578

You can make your code compile, but it will never be usable. Generally, if you see an error which recommends AllowAmbiguosTypes, this is a red herring. It will rarely fix your problem but will sometimes (as in this case) make it seem fixed:

{-# LANGUAGE 
  , ExistentialQuantification
  , TypeFamilies
  , FlexibleInstances
  , FlexibleContexts
  , ScopedTypeVariables
  , AllowAmbiguousTypes #-}

class Monad m => RunableMonad m where
  type ReturnType m :: * -> *
  run :: m a -> ReturnType m a

single :: forall m a . RunableMonad m => a -> ReturnType m a
single x = run (return x :: m a)

But say I have:

import Data.Functor.Identity

instance RunableMonad Identity where 
  type ReturnType Identity = Identity
  run = id

this will produce extremely cryptic errors:

>:t single 'a' :: Identity Char

<interactive>:1:1:
    Couldn't match type `ReturnType m0' with `Identity'
    The type variable `m0' is ambiguous
    Expected type: Identity Char
      Actual type: ReturnType m0 Char
    In the expression: single 'a' :: Identity Char

To see why your function makes no sense, consider

instance RunableMonad [] where 
  type ReturnType [] = Identity
  run = Identity . head 

>:t single 'a'
single 'a' :: RunableMonad m => ReturnType m Char

How do you select which type class instance to use? You may falsely believe that since the m is still present in the type and you still have RunableMonad m, that this type says you can select any m which is a RunableMonad. But since ReturnType is a type function, and type functions are not injective, even if we have ReturnType m Char ~ Identity Char, we can't infer that m ~ Identity - it is obvious that this makes no sense when you take into account the fact that m ~ [] would be a perfectly valid choice here.

It seems to me that the function single should not exist. The fact that the compiler originally rejects it is completely correct, and the fact that you can make it compile with AmbiguousTypes is a misfeature.

If you really must have your single function, you will have to do something like:

class Monad m => RunableMonad m where
  data ReturnType m a
  run :: m a -> ReturnType m a

instance RunableMonad Identity where 
  newtype ReturnType Identity a = RT_Id a deriving Show
  run (Identity a) = RT_Id a 

instance RunableMonad [] where 
  newtype ReturnType [] a = RT_List a deriving Show
  run = RT_List . head 

single x = run (return x) -- type here will be inferred

Upvotes: 2

&#216;rjan Johansen
&#216;rjan Johansen

Reputation: 18189

I think the result from GHCi's :t is essentially wrong in this case, and you will never be able to actually use the expression run $ return x.

The problem is that there is no restriction in your class definition that says that two different Monads m0 and m (to use the same names as your error message) cannot have the same ReturnType.

This means that when looking at the context in which run $ return x is used, GHC might be able to infer what the resulting ReturnType m a is, and from the type of x it can deduce what a is, but it cannot deduce from that what the actual monad m is.

You should however be able to tell it explicitly: run (return x :: WhateverTypeYouReallyWant).

Adding an explicit type annotation should only be necessary when you are using run on an expression like return x which is so polymorphic it can belong to several monads. (Or any monad, in this case.)

Upvotes: 3

thor
thor

Reputation: 22460

I don't have ghc 7.8, so this is only a guess.

I think you can try adding AllowAmbiguousTypes ,as the error message suggests, to 

{-# LANGUAGE ExistentialQuantification, TypeFamilies, FlexibleInstances, FlexibleContexts, ScopedTypeVariables #-}

in the beginning of the source file, or look for a command line option of ghc for compiling with AllowAmbiguousTypes. I had a similar issue with GHCi and ghc command line having different behavior. It turned out that by default, ghci turns on a different set of options than ghc compiler. I ended up solving the problem by ensuring that the compile options and the interpreter options are the same for the feature in question.

Upvotes: 0

Related Questions