Unification of type variables in constraints
The following code works:
{-# LANGUAGE RankNTypes, ConstraintKinds, KindSignatures, GADTs #-}
import Data.Monoid
import GHC.Prim (Constraint)
data Dict :: Constraint -> * where
Dict :: a => Dict a
f :: (c (), c String) => (forall a. Dict (c a) -> a) -> ((), String)
f g = (g Dict, g Dict)
test :: ((), String)
test = f g
where
g :: Dict (Monoid a) -> a
g Dict = mempty
But this doesn't:
f :: (c (), c String) => (forall a. c a => a) -> ((), String)
f g = (g, g)
test :: ((), String)
test = f g
where
g :: Monoid a => a
g = mempty
With the errors:
Could not deduce (c0 String, c0 ()) arising from a use of `f'
Could not deduce (Monoid a) arising from a use of `g'
So it seems that type variables in constraints are not unified. At first I thought this might not be easy to fix, but since there's a workaround I guess it should be possible.
Trac metadata
Trac field | Value |
---|---|
Version | 7.6.1-rc1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |