QuantifiedConstraints: GHC can't infer
This works
{-# Language QuantifiedConstraints, GADTs, KindSignatures, RankNTypes, ConstraintKinds #-}
import Data.Kind
newtype Free :: (Type -> Constraint) -> (Type -> Type) where
Free :: (forall x. cls x => (a -> x) -> x) -> Free cls a
var :: a -> Free cls a
var a = Free $ \var ->
var a
oneTwo :: (forall x. semi x => Semigroup x) => Free semi Int
oneTwo = Free $ \var ->
var 1 <> var 2
nil :: (forall x. mon x => Monoid x) => Free mon Int
nil = Free $ \var ->
mempty
together :: (forall x. mon x => Monoid x) => [Free mon Int]
together = [var 0, nil, oneTwo]
If we comment out together
's type signature GHC cannot infer it back, shouldn't it be able to though?
$ ./ghc-stage2 --interactive -ignore-dot-ghci Proposal.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( Proposal.hs, interpreted )
Proposal.hs:21:20: error:
• Could not deduce (Monoid x) arising from a use of ‘nil’
from the context: cls x
bound by a quantified context at Proposal.hs:21:1-31
Possible fix: add (Monoid x) to the context of a quantified context
• In the expression: nil
In the expression: [var 0, nil, oneTwo]
In an equation for ‘together’: together = [var 0, nil, oneTwo]
|
21 | together = [var 0, nil, oneTwo]
| ^^^
Proposal.hs:21:25: error:
• Could not deduce (Semigroup x) arising from a use of ‘oneTwo’
from the context: cls x
bound by a quantified context at Proposal.hs:21:1-31
Possible fix:
add (Semigroup x) to the context of a quantified context
• In the expression: oneTwo
In the expression: [var 0, nil, oneTwo]
In an equation for ‘together’: together = [var 0, nil, oneTwo]
|
21 | together = [var 0, nil, oneTwo]
| ^^^^^^
Failed, no modules loaded.
Prelude>
Trac metadata
Trac field | Value |
---|---|
Version | 8.5 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |