GHC: Ticket #8053: unification error with ghc head
http://ghc.haskell.org/trac/ghc/ticket/8053
<p>
Ben Gamari is reporting unification errors when he tries to build llvm-general using current GHC HEAD (7.7)
llvm-general currently builds with 7.4 and 7.6, so unless theres substantial changes to how higher rank types are checked, this sounds like it may be a type checker bug in HEAD.
</p>
<p>
<a class="ext-link" href="https://github.com/bscarlet/llvm-general/issues/54"><span class="icon"></span>https://github.com/bscarlet/llvm-general/issues/54</a> is relevant bug report, i'll include a copy of the information in a comment on this ticket
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/8053
Trac 1.2.2.dev0carterThu, 11 Jul 2013 20:57:22 GMT
http://ghc.haskell.org/trac/ghc/ticket/8053#comment:1
http://ghc.haskell.org/trac/ghc/ticket/8053#comment:1
<pre class="wiki">[28 of 96] Compiling Control.Monad.AnyCont.Class ( src/Control/Monad/AnyCont/Class.hs, dist/build/Control/Monad/AnyCont/Class.o )
src/Control/Monad/AnyCont/Class.hs:29:16:
Cannot instantiate unification variable ‛a1’
with a type involving foralls: forall r. (a -> b r) -> b r
Perhaps you want -XImpredicativeTypes
In the expression: lift . anyContToM
In an equation for ‛anyContToM’: anyContToM = lift . anyContToM
In the instance declaration for ‛MonadAnyCont b (StateT s m)’
src/Control/Monad/AnyCont/Class.hs:29:23:
Cannot instantiate unification variable ‛a1’
with a type involving foralls: forall r. (a -> b1 r) -> b1 r
Perhaps you want -XImpredicativeTypes
In the second argument of ‛(.)’, namely ‛anyContToM’
In the expression: lift . anyContToM
src/Control/Monad/AnyCont/Class.hs:36:16:
Cannot instantiate unification variable ‛a0’
with a type involving foralls: forall r. (a -> b r) -> b r
Perhaps you want -XImpredicativeTypes
In the expression: lift . anyContToM
In an equation for ‛anyContToM’: anyContToM = lift . anyContToM
In the instance declaration for ‛MonadAnyCont b (ErrorT e m)’
src/Control/Monad/AnyCont/Class.hs:36:23:
Cannot instantiate unification variable ‛a0’
with a type involving foralls: forall r. (a -> b0 r) -> b0 r
Perhaps you want -XImpredicativeTypes
In the second argument of ‛(.)’, namely ‛anyContToM’
In the expression: lift . anyContToM
Failed to install llvm-general-3.4.0.0
</pre><p>
the relevant modules are
</p>
<pre class="wiki">{-# LANGUAGE
RankNTypes,
MultiParamTypeClasses,
UndecidableInstances
#-}
module Control.Monad.AnyCont.Class where
import Control.Monad.Trans.Class
import Control.Monad.Trans.AnyCont (AnyContT)
import qualified Control.Monad.Trans.AnyCont as AnyCont
import Control.Monad.Trans.Error as Error
import Control.Monad.Trans.State as State
class ScopeAnyCont m where
scopeAnyCont :: m a -> m a
class MonadAnyCont b m where
anyContToM :: (forall r . (a -> b r) -> b r) -> m a
instance MonadTransAnyCont b m => MonadAnyCont b (AnyContT m) where
anyContToM c = AnyCont.anyContT (liftAnyCont c)
instance Monad m => ScopeAnyCont (AnyContT m) where
scopeAnyCont = lift . flip AnyCont.runAnyContT return
instance (Monad m, MonadAnyCont b m) => MonadAnyCont b (StateT s m) where
anyContToM = lift . anyContToM
instance ScopeAnyCont m => ScopeAnyCont (StateT s m) where
scopeAnyCont = StateT . (scopeAnyCont .) . runStateT
instance (Error e, Monad m, MonadAnyCont b m) => MonadAnyCont b (ErrorT e m) where
anyContToM = lift . anyContToM
instance ScopeAnyCont m => ScopeAnyCont (ErrorT e m) where
scopeAnyCont = mapErrorT scopeAnyCont
class MonadTransAnyCont b m where
liftAnyCont :: (forall r . (a -> b r) -> b r) -> (forall r . (a -> m r) -> m r)
instance MonadTransAnyCont b b where
liftAnyCont c = c
instance MonadTransAnyCont b m => MonadTransAnyCont b (StateT s m) where
liftAnyCont c = (\c q -> StateT $ \s -> c $ ($ s) . runStateT . q) (liftAnyCont c)
instance MonadTransAnyCont b m => MonadTransAnyCont b (ErrorT e m) where
liftAnyCont c = (\c q -> ErrorT . c $ runErrorT . q) (liftAnyCont c)
</pre><p>
and
</p>
<pre class="wiki">{-# LANGUAGE
RankNTypes
#-}
module Control.Monad.Trans.AnyCont where
import Control.Applicative
import Control.Monad.Cont
newtype AnyContT m a = AnyContT { unAnyContT :: forall r . ContT r m a }
instance Functor (AnyContT m) where
fmap f p = AnyContT $ fmap f . unAnyContT $ p
instance Applicative (AnyContT m) where
pure a = AnyContT $ pure a
f <*> v = AnyContT $ unAnyContT f <*> unAnyContT v
instance Monad m => Monad (AnyContT m) where
AnyContT f >>= k = AnyContT $ f >>= unAnyContT . k
return a = AnyContT $ return a
fail s = AnyContT (ContT (\_ -> fail s))
instance MonadIO m => MonadIO (AnyContT m) where
liftIO = lift . liftIO
instance MonadTrans AnyContT where
lift ma = AnyContT (lift ma)
runAnyContT :: AnyContT m a -> (forall r . (a -> m r) -> m r)
runAnyContT = runContT . unAnyContT
anyContT :: (forall r . (a -> m r) -> m r) -> AnyContT m a
anyContT f = AnyContT (ContT f)
withAnyContT :: (forall r . (b -> m r) -> (a -> m r)) -> AnyContT m a -> AnyContT m b
withAnyContT f m = anyContT $ runAnyContT m . f
mapAnyContT :: (forall r . m r -> m r) -> AnyContT m a -> AnyContT m a
mapAnyContT f m = anyContT $ f . runAnyContT m
</pre>
TicketthoughtpoliceThu, 11 Jul 2013 21:06:35 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/8053#comment:2
http://ghc.haskell.org/trac/ghc/ticket/8053#comment:2
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>invalid</em>
</li>
</ul>
<p>
This is not a bug. It is the expected behaviour in HEAD. The relevant commit is <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/10f83429ba493699af95cb8c3b16d179d78b7749/ghc" title="Do not instantiate unification variables with polytypes
Without ...">10f83429ba493699af95cb8c3b16d179d78b7749</a>.
</p>
<pre class="wiki">commit 10f83429ba493699af95cb8c3b16d179d78b7749
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date: Wed Oct 31 09:08:39 2012 +0000
Do not instantiate unification variables with polytypes
Without -XImpredicativeTypes, the typing rules say that a function
should be instantiated only at a *monotype*. In implementation terms,
that means that a unification variable should not unify with a type
involving foralls. But we were not enforcing that rule, and that
gave rise to some confusing error messages, such as
Trac #7264, #6069
This patch adds the test for foralls. There are consequences
* I put the test in occurCheckExpand, since that is where we see if a
type can unify with a given unification variable. So
occurCheckExpand has to get DynFlags, so it can test for
-XImpredicativeTypes
* We want this to work
foo :: (forall a. a -> a) -> Int
foo = error "foo"
But that means instantiating error at a polytype! But error is special
already because you can instantiate it at an unboxed type like Int#.
So I extended the specialness to allow type variables of openTypeKind
to unify with polytypes, regardless of -XImpredicativeTypes.
Conveniently, this works in TcUnify.matchExpectedFunTys, which generates
unification variable for the function arguments, which can be polymorphic.
* GHC has a special typing rule for ($) (see Note [Typing rule
for ($)] in TcExpr). It unifies the argument and result with a
unification variable to exclude unboxed types -- but that means I
now need a kind of unificatdion variable that *can* unify with a
polytype.
So for this sole case I added PolyTv to the data type TcType.MetaInfo.
I suspect we'll find mor uses for this, and the changes are tiny,
but it still feel a bit of a hack. Well the special rule for ($)
is a hack!
There were some consequential changes in error reporting (TcErrors).
</pre><p>
The fix is simple, and you don't need ImpredicativeTypes: change the definition of anyContM in the instances from
</p>
<pre class="wiki">anyContToM = lift . anyContToM
</pre><p>
to:
</p>
<pre class="wiki">anyContToM x = lift $ anyContToM x
</pre>
Ticket