GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-01-20T14:59:39Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/15244Ambiguity checks in QuantifiedConstraints2020-01-20T14:59:39ZbitwiseshiftleftAmbiguity checks in QuantifiedConstraintsGreat work on QuantifiedConstraints! I'm giving it a whirl. With GHCI 8.5.20180605, I see somewhat annoying behavior around multiple instances. When two copies of the same (or equivalent) quantified constraint are in scope, they produce ...Great work on QuantifiedConstraints! I'm giving it a whirl. With GHCI 8.5.20180605, I see somewhat annoying behavior around multiple instances. When two copies of the same (or equivalent) quantified constraint are in scope, they produce an error. I think this is about some kind of ambiguity check.
```
{-# LANGUAGE QuantifiedConstraints, TypeFamilies #-}
class (forall t . Eq (c t)) => Blah c
-- Unquantified works
foo :: (Eq (a t), Eq (b t), a ~ b) => a t -> b t -> Bool
foo a b = a == b
-- Works
-- Two quantified instances fail with double ambiguity check errors
bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t -> b t -> Bool
bar a b = a == b
-- Minimal.hs:11:8: error:
-- • Could not deduce (Eq (b t1))
-- from the context: (forall t1. Eq (a t1), forall t1. Eq (b t1),
-- a ~ b)
-- bound by the type signature for:
-- bar :: forall (a :: * -> *) (b :: * -> *) t.
-- (forall t1. Eq (a t1), forall t1. Eq (b t1), a ~ b) =>
-- a t -> b t -> Bool
-- at Minimal.hs:11:8-78
-- • In the ambiguity check for ‘bar’
-- To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-- In the type signature:
-- bar :: (forall t. Eq (a t), forall t. Eq (b t), a ~ b) =>
-- a t -> b t -> Bool
-- |
-- 11 | bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t -> b t -> Bool
-- |
-- [And then another copy of the same error]
-- Two copies from superclass instances fail
baz :: (Blah a, Blah b, a ~ b) => a t -> b t -> Bool
baz a b = a == b
-- Minimal.hs:34:11: error:
-- • Could not deduce (Eq (b t)) arising from a use of ‘==’
-- from the context: (Blah a, Blah b, a ~ b)
-- bound by the type signature for:
-- baz :: forall (a :: * -> *) (b :: * -> *) t.
-- (Blah a, Blah b, a ~ b) =>
-- a t -> b t -> Bool
-- at Minimal.hs:33:1-52
-- • In the expression: a == b
-- In an equation for ‘baz’: baz a b = a == b
-- |
-- 34 | baz a b = a == b
-- |
-- Two copies from superclass from same declaration also fail
mugga :: (Blah a, Blah a) => a t -> a t -> Bool
mugga a b = a == b
-- • Could not deduce (Eq (a t)) arising from a use of ‘==’
-- from the context: (Blah a, Blah a)
-- bound by the type signature for:
-- mugga :: forall (a :: * -> *) t.
-- (Blah a, Blah a) =>
-- a t -> a t -> Bool
-- at Minimal.hs:50:1-47
-- • In the expression: a == b
-- In an equation for ‘mugga’: mugga a b = a == b
-- |
-- 51 | mugga a b = a == b
-- |
-- One copy works
quux :: (Blah a, a ~ b) => a t -> b t -> Bool
quux a b = a == b
-- Works
```
My program is similar to `Baz`. The constraints `Blah a` and `Blah b` are in scope from a pattern match, and I want to compare values of types `a t` and `b t` if they're the same type. So I get `a ~ b` from Typeable and try to compare them, but this doesn't work. I worked around the issue by writing a helper that only takes `(Blah a, Typeable a, Typeable b)`, so only one instance is in scope.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Ambiguity checks in QuantifiedConstraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Great work on QuantifiedConstraints! I'm giving it a whirl. With GHCI 8.5.20180605, I see somewhat annoying behavior around multiple instances. When two copies of the same (or equivalent) quantified constraint are in scope, they produce an error. I think this is about some kind of ambiguity check.\r\n\r\n{{{\r\n{-# LANGUAGE QuantifiedConstraints, TypeFamilies #-}\r\n\r\nclass (forall t . Eq (c t)) => Blah c\r\n\r\n-- Unquantified works\r\nfoo :: (Eq (a t), Eq (b t), a ~ b) => a t -> b t -> Bool\r\nfoo a b = a == b\r\n-- Works\r\n \r\n-- Two quantified instances fail with double ambiguity check errors\r\nbar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t -> b t -> Bool\r\nbar a b = a == b\r\n-- Minimal.hs:11:8: error:\r\n-- • Could not deduce (Eq (b t1))\r\n-- from the context: (forall t1. Eq (a t1), forall t1. Eq (b t1),\r\n-- a ~ b)\r\n-- bound by the type signature for:\r\n-- bar :: forall (a :: * -> *) (b :: * -> *) t.\r\n-- (forall t1. Eq (a t1), forall t1. Eq (b t1), a ~ b) =>\r\n-- a t -> b t -> Bool\r\n-- at Minimal.hs:11:8-78\r\n-- • In the ambiguity check for ‘bar’\r\n-- To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n-- In the type signature:\r\n-- bar :: (forall t. Eq (a t), forall t. Eq (b t), a ~ b) =>\r\n-- a t -> b t -> Bool\r\n-- |\r\n-- 11 | bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t -> b t -> Bool\r\n-- |\r\n-- [And then another copy of the same error]\r\n\r\n-- Two copies from superclass instances fail\r\nbaz :: (Blah a, Blah b, a ~ b) => a t -> b t -> Bool\r\nbaz a b = a == b\r\n-- Minimal.hs:34:11: error:\r\n-- • Could not deduce (Eq (b t)) arising from a use of ‘==’\r\n-- from the context: (Blah a, Blah b, a ~ b)\r\n-- bound by the type signature for:\r\n-- baz :: forall (a :: * -> *) (b :: * -> *) t.\r\n-- (Blah a, Blah b, a ~ b) =>\r\n-- a t -> b t -> Bool\r\n-- at Minimal.hs:33:1-52\r\n-- • In the expression: a == b\r\n-- In an equation for ‘baz’: baz a b = a == b\r\n-- |\r\n-- 34 | baz a b = a == b\r\n-- | \r\n\r\n-- Two copies from superclass from same declaration also fail\r\nmugga :: (Blah a, Blah a) => a t -> a t -> Bool\r\nmugga a b = a == b\r\n-- • Could not deduce (Eq (a t)) arising from a use of ‘==’\r\n-- from the context: (Blah a, Blah a)\r\n-- bound by the type signature for:\r\n-- mugga :: forall (a :: * -> *) t.\r\n-- (Blah a, Blah a) =>\r\n-- a t -> a t -> Bool\r\n-- at Minimal.hs:50:1-47\r\n-- • In the expression: a == b\r\n-- In an equation for ‘mugga’: mugga a b = a == b\r\n-- |\r\n-- 51 | mugga a b = a == b\r\n-- |\r\n\r\n-- One copy works\r\nquux :: (Blah a, a ~ b) => a t -> b t -> Bool\r\nquux a b = a == b\r\n-- Works\r\n}}}\r\n\r\nMy program is similar to {{{Baz}}}. The constraints {{{Blah a}}} and {{{Blah b}}} are in scope from a pattern match, and I want to compare values of types {{{a t}}} and {{{b t}}} if they're the same type. So I get {{{a ~ b}}} from Typeable and try to compare them, but this doesn't work. I worked around the issue by writing a helper that only takes {{{(Blah a, Typeable a, Typeable b)}}}, so only one instance is in scope.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15290QuantifiedConstraints: panic "addTcEvBind NoEvBindsVar"2024-01-11T02:06:42ZRichard Eisenbergrae@richarde.devQuantifiedConstraints: panic "addTcEvBind NoEvBindsVar"I wanted to see if we're ready to put `join` into `Monad`. So I typed this in:
```hs
{-# LANGUAGE QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-}
module Bug where
import Prelude hiding ( Monad(..) )
import Da...I wanted to see if we're ready to put `join` into `Monad`. So I typed this in:
```hs
{-# LANGUAGE QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-}
module Bug where
import Prelude hiding ( Monad(..) )
import Data.Coerce ( Coercible )
class Monad m where
(>>=) :: m a -> (a -> m b) -> m b
join :: m (m a) -> m a
newtype StateT s m a = StateT { runStateT :: s -> m (s, a) }
instance Monad m => Monad (StateT s m) where
ma >>= fmb = StateT $ \s -> runStateT ma s >>= \(s1, a) -> runStateT (fmb a) s1
join ssa = StateT $ \s -> runStateT ssa s >>= \(s, sa) -> runStateT sa s
newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }
deriving instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q)) => Monad (IntStateT m)
```
This looks like it should be accepted. But I get
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.5.20180617 for x86_64-apple-darwin):
addTcEvBind NoEvBindsVar
[G] df_a67k
= \ (@ p_a62C) (@ q_a62D) (v_B1 :: Coercible p_a62C q_a62D) ->
coercible_sel
@ *
@ (m_a64Z[ssk:1] p_a62C)
@ (m_a64Z[ssk:1] q_a62D)
(df_a651 @ p_a62C @ q_a62D v_B1)
a67c
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcRnMonad.hs:1404:5 in ghc:TcRnMonad
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"QuantifiedConstraints: panic \"addTcEvBind NoEvBindsVar\"","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I wanted to see if we're ready to put `join` into `Monad`. So I typed this in:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-}\r\n\r\nmodule Bug where\r\n\r\nimport Prelude hiding ( Monad(..) )\r\nimport Data.Coerce ( Coercible )\r\n\r\nclass Monad m where\r\n (>>=) :: m a -> (a -> m b) -> m b\r\n join :: m (m a) -> m a\r\n\r\nnewtype StateT s m a = StateT { runStateT :: s -> m (s, a) }\r\n\r\ninstance Monad m => Monad (StateT s m) where\r\n ma >>= fmb = StateT $ \\s -> runStateT ma s >>= \\(s1, a) -> runStateT (fmb a) s1\r\n join ssa = StateT $ \\s -> runStateT ssa s >>= \\(s, sa) -> runStateT sa s\r\n\r\nnewtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }\r\n\r\nderiving instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q)) => Monad (IntStateT m)\r\n\r\n}}}\r\n\r\nThis looks like it should be accepted. But I get\r\n\r\n{{{\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180617 for x86_64-apple-darwin):\r\n\taddTcEvBind NoEvBindsVar\r\n [G] df_a67k\r\n = \\ (@ p_a62C) (@ q_a62D) (v_B1 :: Coercible p_a62C q_a62D) ->\r\n coercible_sel\r\n @ *\r\n @ (m_a64Z[ssk:1] p_a62C)\r\n @ (m_a64Z[ssk:1] q_a62D)\r\n (df_a651 @ p_a62C @ q_a62D v_B1)\r\n a67c\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcRnMonad.hs:1404:5 in ghc:TcRnMonad\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15507Deriving with QuantifiedConstraints is unable to penetrate type families2019-07-07T18:04:26ZisovectorDeriving with QuantifiedConstraints is unable to penetrate type familiesI'd expect the following code to successfully derive a usable `Eq` instance for `Foo`.
```hs
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAG...I'd expect the following code to successfully derive a usable `Eq` instance for `Foo`.
```hs
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module QuantifiedConstraints where
import Data.Functor.Identity
type family HKD f a where
HKD Identity a = a
HKD f a = f a
data Foo f = Foo
{ zoo :: HKD f Int
, zum :: HKD f Bool
}
deriving instance (forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)
```
However, it complains:
```
• Could not deduce (Eq (HKD f a))
from the context: forall a. Eq a => Eq (HKD f a)
bound by an instance declaration:
forall (f :: * -> *).
(forall a. Eq a => Eq (HKD f a)) =>
Eq (Foo f)
at /home/sandy/prj/book-of-types/code/QuantifiedConstraints.hs:20:19-64
or from: Eq a
bound by a quantified context
at /home/sandy/prj/book-of-types/code/QuantifiedConstraints.hs:20:19-64
• In the ambiguity check for an instance declaration
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the stand-alone deriving instance for
‘(forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)’
```
Adding -XAllowAmbiguousTypes doesn't fix the situation:
```
• Could not deduce (Eq (HKD f Int)) arising from a use of ‘==’
from the context: forall a. Eq a => Eq (HKD f a)
bound by the instance declaration
at /home/sandy/prj/book-of-types/code/QuantifiedConstraints.hs:21:1-64
• In the first argument of ‘(&&)’, namely ‘((a1 == b1))’
In the expression: (((a1 == b1)) && ((a2 == b2)))
In an equation for ‘==’:
(==) (Foo a1 a2) (Foo b1 b2) = (((a1 == b1)) && ((a2 == b2)))
When typechecking the code for ‘==’
in a derived instance for ‘Eq (Foo f)’:
To see the code I am typechecking, use -ddump-deriv
|
21 | deriving instance (forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
/home/sandy/prj/book-of-types/code/QuantifiedConstraints.hs:21:1: error:
• Could not deduce (Eq (HKD f a))
arising from a use of ‘GHC.Classes.$dm/=’
from the context: forall a. Eq a => Eq (HKD f a)
bound by the instance declaration
at /home/sandy/prj/book-of-types/code/QuantifiedConstraints.hs:21:1-64
or from: Eq a
bound by a quantified context
at /home/sandy/prj/book-of-types/code/QuantifiedConstraints.hs:1:1
• In the expression: GHC.Classes.$dm/= @(Foo f)
In an equation for ‘/=’: (/=) = GHC.Classes.$dm/= @(Foo f)
When typechecking the code for ‘/=’
in a derived instance for ‘Eq (Foo f)’:
To see the code I am typechecking, use -ddump-deriv
In the instance declaration for ‘Eq (Foo f)’
|
21 | deriving instance (forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
and the result of -ddump-deriv:
```
==================== Derived instances ====================
Derived class instances:
instance (forall a.
GHC.Classes.Eq a =>
GHC.Classes.Eq (QuantifiedConstraints.HKD f a)) =>
GHC.Classes.Eq (QuantifiedConstraints.Foo f) where
(GHC.Classes.==)
(QuantifiedConstraints.Foo a1_a74s a2_a74t)
(QuantifiedConstraints.Foo b1_a74u b2_a74v)
= (((a1_a74s GHC.Classes.== b1_a74u))
GHC.Classes.&& ((a2_a74t GHC.Classes.== b2_a74v)))
Derived type family instances:
==================== Filling in method body ====================
GHC.Classes.Eq [QuantifiedConstraints.Foo f_a74w[ssk:1]]
GHC.Classes./= = GHC.Classes.$dm/=
@(QuantifiedConstraints.Foo f_a74w[ssk:1])
```8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15593QuantifiedConstraints: trouble with type family2019-07-07T18:03:59ZIcelandjackQuantifiedConstraints: trouble with type family```hs
{-# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances #-}
import Data.Kind
data TreeF a b = T0 | T1 a | T2 b b
-- from Data.Reify
class MuRef (a :: Type) where
type DeRef a :: Type -> Type
class ...```hs
{-# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances #-}
import Data.Kind
data TreeF a b = T0 | T1 a | T2 b b
-- from Data.Reify
class MuRef (a :: Type) where
type DeRef a :: Type -> Type
class (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree
instance (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree
```
fails with
```
$ ~/code/qc-ghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 351.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 351.hs, interpreted )
351.hs:12:10: error:
• Couldn't match type ‘DeRef (tree xx)’ with ‘TreeF xx’
arising from the superclasses of an instance declaration
• In the instance declaration for ‘MuRef1 tree’
|
12 | instance (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude>
```
----
What I want to write:
```hs
{-# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances, DataKinds, TypeInType, MultiParamTypeClasses, UndecidableInstances, AllowAmbiguousTypes #-}
import Data.Kind
-- from Data.Reify
class MuRef (a :: Type) where
type DeRef a :: Type -> Type
type T = Type
type TT = T -> T
type TTT = T -> TT
class (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx)) => MuRef1 (f :: TT) (deRef1 :: TT -> TTT)
instance (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx)) => MuRef1 (f :: TT) (deRef1 :: TT -> TTT)
```
where I am trying to capture [MuRef1 & DeRef1](https://hackage.haskell.org/package/folds-0.7.4/docs/src/Data-Fold-Internal.html)
```hs
class MuRef1 (f :: TT) where
type DeRef1 f :: TTT
muRef1 :: proxy (f a) -> Dict (MuRef (f a), DeRef (f a) ~ DeRef1 f a)
```
----
Workarounds: I think splitting the class alias & quantification does the job (I haven't tested it but it compiles), I want to know if the first two programs are meant to compile or not
```hs
{-# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances, DataKinds, TypeInType, MultiParamTypeClasses, UndecidableInstances, AllowAmbiguousTypes, FlexibleContexts #-}
-- ..
class (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx
instance (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx
class (forall xx. cls xx) => Forall cls
instance (forall xx. cls xx) => Forall cls
class Forall (MuRef1_ f deRef1) => MuRef1 f deRef1
instance Forall (MuRef1_ f deRef1) => MuRef1 f deRef1
```
or as a regular type/constraint synonym (at the loss of partial application)
```hs
type MuRef1 f deRef1 = (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx))
```
<details><summary>Trac metadata</summary>
| 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 | |
</details>
<!-- {"blocked_by":[],"summary":"QuantifiedConstraints: trouble with type family","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["ConstraintKinds","QuantifiedConstraints,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances #-}\r\n\r\nimport Data.Kind\r\n\r\ndata TreeF a b = T0 | T1 a | T2 b b\r\n\r\n-- from Data.Reify\r\nclass MuRef (a :: Type) where\r\n type DeRef a :: Type -> Type\r\n\r\nclass (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree\r\ninstance (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree\r\n}}}\r\n\r\nfails with\r\n\r\n{{{\r\n$ ~/code/qc-ghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 351.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 351.hs, interpreted )\r\n\r\n351.hs:12:10: error:\r\n • Couldn't match type ‘DeRef (tree xx)’ with ‘TreeF xx’\r\n arising from the superclasses of an instance declaration\r\n • In the instance declaration for ‘MuRef1 tree’\r\n |\r\n12 | instance (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\n----\r\n\r\nWhat I want to write:\r\n\r\n{{{#!hs\r\n{-# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances, DataKinds, TypeInType, MultiParamTypeClasses, UndecidableInstances, AllowAmbiguousTypes #-}\r\n\r\nimport Data.Kind\r\n\r\n-- from Data.Reify\r\nclass MuRef (a :: Type) where\r\n type DeRef a :: Type -> Type\r\n\r\ntype T = Type\r\ntype TT = T -> T\r\ntype TTT = T -> TT\r\n\r\nclass (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx)) => MuRef1 (f :: TT) (deRef1 :: TT -> TTT)\r\ninstance (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx)) => MuRef1 (f :: TT) (deRef1 :: TT -> TTT)\r\n}}}\r\n\r\nwhere I am trying to capture [https://hackage.haskell.org/package/folds-0.7.4/docs/src/Data-Fold-Internal.html MuRef1 & DeRef1]\r\n\r\n{{{#!hs\r\nclass MuRef1 (f :: TT) where\r\n type DeRef1 f :: TTT\r\n muRef1 :: proxy (f a) -> Dict (MuRef (f a), DeRef (f a) ~ DeRef1 f a)\r\n}}}\r\n\r\n----\r\n\r\nWorkarounds: I think splitting the class alias & quantification does the job (I haven't tested it but it compiles), I want to know if the first two programs are meant to compile or not\r\n\r\n{{{#!hs\r\n{-# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances, DataKinds, TypeInType, MultiParamTypeClasses, UndecidableInstances, AllowAmbiguousTypes, FlexibleContexts #-}\r\n\r\n-- ..\r\n\r\nclass (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx\r\ninstance (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx\r\n\r\nclass (forall xx. cls xx) => Forall cls\r\ninstance (forall xx. cls xx) => Forall cls\r\n\r\nclass Forall (MuRef1_ f deRef1) => MuRef1 f deRef1\r\ninstance Forall (MuRef1_ f deRef1) => MuRef1 f deRef1\r\n}}}\r\n\r\nor as a regular type/constraint synonym (at the loss of partial application)\r\n\r\n{{{#!hs\r\ntype MuRef1 f deRef1 = (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx))\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15635Implication introduction for quantified constraints2019-07-07T18:03:39ZDavid FeuerImplication introduction for quantified constraintsNow that we have `QuantifiedConstraints`, it seems we need some implication introduction form. The `constraints` package has these types:
```hs
data Dict a where
Dict :: a => Dict a
newtype a :- b = Sub (a => Dict b)
```
`Quantified...Now that we have `QuantifiedConstraints`, it seems we need some implication introduction form. The `constraints` package has these types:
```hs
data Dict a where
Dict :: a => Dict a
newtype a :- b = Sub (a => Dict b)
```
`QuantifiedConstraints` suggests another version of `:-`:
```hs
newtype Imp a b = Imp
{ unImp :: forall r. ((a => b) => r) -> r}
```
We can write
```hs
fromImp :: Imp a b -> a :- b
fromImp (Imp f) = Sub (f Dict)
```
But ... there's no way to go the other way!
Let's try it:
```hs
toImp :: a :- Dict b -> a :- b
toImp (Sub ab) = Imp $ \r -> _
```
We get
```
* Found hole: _ :: r
* Relevant bindings include
r :: (a => b) => r
ab :: a => Dict b
```
There's no way to put these things together. But there's no terribly obvious reason they ''can't* be combined. `a => b` is a function from an `a` dictionary to a `b` dictionary. `a => Dict b` is a function from an `a` dictionary to a value that *contains'' a `b` dictionary. We just need some way to plumb these things together: some sort of implication introduction. The simplest thing might be a bit of magic:
```hs
implIntro
:: ((a => b) => q)
-> (forall r. (b => r) -> (a => r))
-> q
```
In Core (modulo type abstraction and application), we could simply write
```hs
implIntro f g = f (g id)
```
Unfortunately, I doubt that `implIntro` is really general enough to do everything people will want in this space.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.6.1-beta1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Implication introduction for quantified constraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1-beta1","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Now that we have `QuantifiedConstraints`, it seems we need some implication introduction form. The `constraints` package has these types:\r\n\r\n{{{#!hs\r\ndata Dict a where\r\n Dict :: a => Dict a\r\n\r\nnewtype a :- b = Sub (a => Dict b)\r\n}}}\r\n\r\n`QuantifiedConstraints` suggests another version of `:-`:\r\n\r\n{{{#!hs\r\nnewtype Imp a b = Imp\r\n { unImp :: forall r. ((a => b) => r) -> r}\r\n}}}\r\n\r\nWe can write\r\n\r\n{{{#!hs\r\nfromImp :: Imp a b -> a :- b\r\nfromImp (Imp f) = Sub (f Dict)\r\n}}}\r\n\r\nBut ... there's no way to go the other way!\r\n\r\nLet's try it:\r\n\r\n{{{#!hs\r\ntoImp :: a :- Dict b -> a :- b\r\ntoImp (Sub ab) = Imp $ \\r -> _\r\n}}}\r\n\r\nWe get\r\n\r\n{{{\r\n* Found hole: _ :: r\r\n* Relevant bindings include\r\n r :: (a => b) => r\r\n ab :: a => Dict b\r\n}}}\r\n\r\nThere's no way to put these things together. But there's no terribly obvious reason they ''can't'' be combined. `a => b` is a function from an `a` dictionary to a `b` dictionary. `a => Dict b` is a function from an `a` dictionary to a value that ''contains'' a `b` dictionary. We just need some way to plumb these things together: some sort of implication introduction. The simplest thing might be a bit of magic:\r\n\r\n{{{#!hs\r\nimplIntro\r\n :: ((a => b) => q)\r\n -> (forall r. (b => r) -> (a => r))\r\n -> q\r\n}}}\r\n\r\nIn Core (modulo type abstraction and application), we could simply write\r\n\r\n{{{#!hs\r\nimplIntro f g = f (g id)\r\n}}}\r\n\r\nUnfortunately, I doubt that `implIntro` is really general enough to do everything people will want in this space.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15636Implication constraint priority breaks default class implementations2019-07-07T18:03:39Zi-am-tomImplication constraint priority breaks default class implementationsHello,
Not 100% sure that this is a bug, but I've done some investigating (with a *lot* of help from Csongor Kiss) and thought it was, at the very least, behaviour worth clarifying. The following code...
```hs
{-# LANGUAGE FlexibleInst...Hello,
Not 100% sure that this is a bug, but I've done some investigating (with a *lot* of help from Csongor Kiss) and thought it was, at the very least, behaviour worth clarifying. The following code...
```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module Test where
class D a where
f :: a -> String
g :: a -> String
g = f
class C a
instance (forall a. C a => D a) => D x where
f _ = "uh oh"
```
1. .. produces the error:
```
• Could not deduce (C x) arising from a use of ‘Test.$dmg’
from the context: forall a. C a => D a
bound by the instance declaration at Test.hs:19:10-38
Possible fix: add (C x) to the context of the instance declaration
• In the expression: Test.$dmg @(x)
In an equation for ‘g’: g = Test.$dmg @(x)
In the instance declaration for ‘D x’
|
19 | instance (forall a. C a => D a) => D x where
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
It appears that the problem here is with the default implementation for `g`. Namely, when `f` is called, two matching instances are found:
- `forall a. C a => D a`
- `(forall a. C a => D a) => D x`
The issue, as far as we can tell, is that the first instance is chosen (and then the constraint check fails). I'm currently working around this by introducing a newtype into the head of the quantified constraint†, but I thought it best to check whether this is a bug or, indeed, the expected behaviour in this situation.
Let me know if I've missed anything from this ticket - it's my first one!
Thanks,
Tom
† An example of this can be found at https://github.com/i-am-tom/learn-me-a-haskell/blob/dbf2a22c5abb78ab91124dcf1e0e7ecd3d88831d/src/Bag/QuantifiedInstances.hs\#L92-L94
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1-beta1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Implication constraint priority breaks default class implementations","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1-beta1","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Hello,\r\n\r\nNot 100% sure that this is a bug, but I've done some investigating (with a ''lot'' of help from Csongor Kiss) and thought it was, at the very least, behaviour worth clarifying. The following code...\r\n\r\n{{{#!hs\r\n{-# LANGUAGE FlexibleInstances #-}\r\n{-# LANGUAGE QuantifiedConstraints #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule Test where\r\n\r\nclass D a where\r\n f :: a -> String\r\n g :: a -> String\r\n g = f\r\n\r\nclass C a\r\n\r\ninstance (forall a. C a => D a) => D x where\r\n f _ = \"uh oh\"\r\n}}}\r\n\r\n... produces the error:\r\n\r\n{{{\r\n • Could not deduce (C x) arising from a use of ‘Test.$dmg’\r\n from the context: forall a. C a => D a\r\n bound by the instance declaration at Test.hs:19:10-38\r\n Possible fix: add (C x) to the context of the instance declaration\r\n • In the expression: Test.$dmg @(x)\r\n In an equation for ‘g’: g = Test.$dmg @(x)\r\n In the instance declaration for ‘D x’\r\n |\r\n19 | instance (forall a. C a => D a) => D x where\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nIt appears that the problem here is with the default implementation for `g`. Namely, when `f` is called, two matching instances are found:\r\n\r\n- `forall a. C a => D a`\r\n- `(forall a. C a => D a) => D x`\r\n\r\nThe issue, as far as we can tell, is that the first instance is chosen (and then the constraint check fails). I'm currently working around this by introducing a newtype into the head of the quantified constraint†, but I thought it best to check whether this is a bug or, indeed, the expected behaviour in this situation.\r\n\r\nLet me know if I've missed anything from this ticket - it's my first one!\r\n\r\nThanks,\r\nTom\r\n\r\n† An example of this can be found at https://github.com/i-am-tom/learn-me-a-haskell/blob/dbf2a22c5abb78ab91124dcf1e0e7ecd3d88831d/src/Bag/QuantifiedInstances.hs#L92-L94","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1