GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200714T14:19:56Zhttps://gitlab.haskell.org/ghc/ghc//issues/18406Functional dependency should constrain local inferred type, but does not20200714T14:19:56ZRichard Eisenbergrae@richarde.devFunctional dependency should constrain local inferred type, but does notIf I compile
```hs
{# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #}
module Bug where
class C a b  a > b where
op :: a > a
foo :: C a b => a > b > a
foo x y = blah x
where
blah z = [x,z] `seq` op z
```
with `ddumptc fprinttypecheckerelaboration fprintexplicitforalls`, I get
```
==================== Typechecker ====================
AbsBinds [a_apDT, b_apDU] [$dC_apDW]
{Exports: [foo <= foo_apDV
wrap: <>]
Exported types: foo :: forall a b. C a b => a > b > a
[LclId]
Binds: foo_apDV x_apD6 y_apD7
= blah_apD8 @ b_apDU $dC_apEm x_apD6
where
AbsBinds [b_apE7] [$dC_apEd]
{Exports: [blah_apD8 <= blah_apEb
wrap: <>]
Exported types: blah_apD8
:: forall {b}. C a_apDT b => a_apDT > a_apDT
[LclId]
Binds: blah_apD8 z_apD9
= [x_apD6, z_apD9] `seq` op @ a_apDT @ b_apE7 $dC_apE8 z_apD9
Evidence: [EvBinds{[W] $dC_apE8 = $dC_apEd}]}
Evidence: [EvBinds{[W] $dC_apEm = $dC_apDW}]}
```
Note that the local `blah` gets type `forall {b}. C a b => a > a`. Why quantify `b` locally? There is no reason to. There is no great harm either, but a patch I'm working on (https://gitlab.haskell.org/ghc/ghc//tree/wip/derivedrefactor) gets annoyed when this condition (which happens in the wild, in `Text.Parsec.Perm`) causes `[G] C a b1` and `[G] C a b2` to both be in scope with no relationship between `b1` and `b2`.
Will fix in ongoing work.If I compile
```hs
{# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #}
module Bug where
class C a b  a > b where
op :: a > a
foo :: C a b => a > b > a
foo x y = blah x
where
blah z = [x,z] `seq` op z
```
with `ddumptc fprinttypecheckerelaboration fprintexplicitforalls`, I get
```
==================== Typechecker ====================
AbsBinds [a_apDT, b_apDU] [$dC_apDW]
{Exports: [foo <= foo_apDV
wrap: <>]
Exported types: foo :: forall a b. C a b => a > b > a
[LclId]
Binds: foo_apDV x_apD6 y_apD7
= blah_apD8 @ b_apDU $dC_apEm x_apD6
where
AbsBinds [b_apE7] [$dC_apEd]
{Exports: [blah_apD8 <= blah_apEb
wrap: <>]
Exported types: blah_apD8
:: forall {b}. C a_apDT b => a_apDT > a_apDT
[LclId]
Binds: blah_apD8 z_apD9
= [x_apD6, z_apD9] `seq` op @ a_apDT @ b_apE7 $dC_apE8 z_apD9
Evidence: [EvBinds{[W] $dC_apE8 = $dC_apEd}]}
Evidence: [EvBinds{[W] $dC_apEm = $dC_apDW}]}
```
Note that the local `blah` gets type `forall {b}. C a b => a > a`. Why quantify `b` locally? There is no reason to. There is no great harm either, but a patch I'm working on (https://gitlab.haskell.org/ghc/ghc//tree/wip/derivedrefactor) gets annoyed when this condition (which happens in the wild, in `Text.Parsec.Perm`) causes `[G] C a b1` and `[G] C a b2` to both be in scope with no relationship between `b1` and `b2`.
Will fix in ongoing work.https://gitlab.haskell.org/ghc/ghc//issues/18400Instances do not respect functional dependency, yet are accepted20200705T16:37:39ZRichard Eisenbergrae@richarde.devInstances do not respect functional dependency, yet are acceptedTaken from #7875:
```hs
class Het a b  a > b where
het :: m (f c) > a > m b
class GHet (a :: Type > Type) (b :: Type > Type)  a > b
instance GHet (K a) (K [a])
instance Het a b => GHet (K a) (K b)
data K x a = K x
```
Ticket #7875 is about a problem that arises later... but I'm flummoxed as to why these instances are accepted. The two instances of `GHet` seem quite assuredly to violate its fundep. Yet ticket #7875 seems unconcerned about this issue, so I'm reluctant to fix until someone agrees that these instances are indeed problematic. Help?Taken from #7875:
```hs
class Het a b  a > b where
het :: m (f c) > a > m b
class GHet (a :: Type > Type) (b :: Type > Type)  a > b
instance GHet (K a) (K [a])
instance Het a b => GHet (K a) (K b)
data K x a = K x
```
Ticket #7875 is about a problem that arises later... but I'm flummoxed as to why these instances are accepted. The two instances of `GHet` seem quite assuredly to violate its fundep. Yet ticket #7875 seems unconcerned about this issue, so I'm reluctant to fix until someone agrees that these instances are indeed problematic. Help?https://gitlab.haskell.org/ghc/ghc//issues/18398Inferred type too general, ignoring functional dependencies20200705T16:35:51ZRichard Eisenbergrae@richarde.devInferred type too general, ignoring functional dependenciesConsider
```hs
module FloatFDs2 where
class C a b  a > b where
meth :: a > b > ()
data Ex where
MkEx :: a > Ex
f x = (\y > case x of MkEx _ > meth x y, \z > case x of MkEx _ > meth x z)
```
GHC infers `f :: forall p1 p2. (C Ex p1, C Ex p2) => Ex > (p1 > (), p2 > ())`. That's silly: `p1` and `p2` should have been unified.
Solution is on the way in a branch I'm working on about a constraint solver refactor.Consider
```hs
module FloatFDs2 where
class C a b  a > b where
meth :: a > b > ()
data Ex where
MkEx :: a > Ex
f x = (\y > case x of MkEx _ > meth x y, \z > case x of MkEx _ > meth x z)
```
GHC infers `f :: forall p1 p2. (C Ex p1, C Ex p2) => Ex > (p1 > (), p2 > ())`. That's silly: `p1` and `p2` should have been unified.
Solution is on the way in a branch I'm working on about a constraint solver refactor.https://gitlab.haskell.org/ghc/ghc//issues/17765Documentation for FunctionalDependencies is misleading/incomplete (and their ...20200220T16:51:39ZJakob BrünkerDocumentation for FunctionalDependencies is misleading/incomplete (and their behavior confusing) wrt overlapping instances## Summary
The GHC user's guide mentions in *9.8.2.2.2. Adding functional dependencies*, for `class D a b  a > b where ...`:
> The compiler, on the other hand, is responsible for ensuring that the set of instances that are in scope at any given point in the program is consistent with any declared dependencies. For example, the following pair of instance declarations cannot appear together in the same scope because they violate the dependency for D, even though either one on its own would be acceptable:
>
> ```haskell
> instance D Bool Int where ...
> instance D Bool Char where ...
> ```
This leaves out what happens when polymorphic types are used in instances, and some of the behavior of functional dependencies in that case is not what I would expect judging by the documentation, but I suspect that they work as intended.
To illustrate:
```haskell
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE FlexibleInstances #}
module FunDeps where
class C a b  a > b where
foo :: a > b
 It is unclear to me why I can write both of these instances together  it
 seems as though this should violate the dependency
instance C a a where
foo = id
instance C a () where
foo = const ()
 understandably not fine, due to Overlapping instances
 ex0 = foo () :: ()
 fine
ex1 = foo 'x' :: Char
 also fine
 However, the User's guide says "The notation `a > b` [...] indicates that the `a`
 parameter uniquely determines the `b` parameter, and might be read as “a determines b.”"
 From this I would expect that an expression like `foo 'x'` has a uniquely determined
 type, but evidently, this is not so, since it can have both type `Char` and `()`.
ex2 = foo 'x' :: ()
 not fine, with confusing error message
 Why does it expect the argument of `foo` to be of type `()` when, with
 an annotation, it accepts a `Char` argument?
 In fact, it looks like it selected the `C a a` instance and from it determined that
 it needs to solve a `C Char ()` constraint, which seems paradoxical.
 Naively I would expect GHC to talk about an ambiguous type variable, which
 is what happens if the functional dependency is removed.
ex3 = foo 'x'
{
FunDeps.hs:25:7: error:
• Couldn't match type ‘Char’ with ‘()’
arising from a functional dependency between:
constraint ‘C Char ()’ arising from a use of ‘foo’
instance ‘C a a’ at FunDeps.hs:9:1014
• In the expression: foo 'x'
In an equation for ‘ex3’: ex3 = foo 'x'

25  ex3 = foo 'x'
 ^^^^^^^
}
```
Another interesting aspect is that entering `() :: C Bool () => ()` in GHCi will produce the exact same warning twice, though I don't know if that's expected behavior:
```haskell
<interactive>:45:7: warning: [Wsimplifiableclassconstraints]
• The constraint ‘C Bool ()’ matches
instance C a ()  Defined at FunDeps.hs:15:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In an expression type signature: C Bool () => ()
In the expression: () :: C Bool () => ()
In an equation for ‘it’: it = () :: C Bool () => ()
<interactive>:45:7: warning: [Wsimplifiableclassconstraints]
• The constraint ‘C Bool ()’ matches
instance C a ()  Defined at FunDeps.hs:15:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In an expression type signature: C Bool () => ()
In the expression: () :: C Bool () => ()
In an equation for ‘it’: it = () :: C Bool () => ()
```
## Environment
* GHC version used: 8.11.0.20200127## Summary
The GHC user's guide mentions in *9.8.2.2.2. Adding functional dependencies*, for `class D a b  a > b where ...`:
> The compiler, on the other hand, is responsible for ensuring that the set of instances that are in scope at any given point in the program is consistent with any declared dependencies. For example, the following pair of instance declarations cannot appear together in the same scope because they violate the dependency for D, even though either one on its own would be acceptable:
>
> ```haskell
> instance D Bool Int where ...
> instance D Bool Char where ...
> ```
This leaves out what happens when polymorphic types are used in instances, and some of the behavior of functional dependencies in that case is not what I would expect judging by the documentation, but I suspect that they work as intended.
To illustrate:
```haskell
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE FlexibleInstances #}
module FunDeps where
class C a b  a > b where
foo :: a > b
 It is unclear to me why I can write both of these instances together  it
 seems as though this should violate the dependency
instance C a a where
foo = id
instance C a () where
foo = const ()
 understandably not fine, due to Overlapping instances
 ex0 = foo () :: ()
 fine
ex1 = foo 'x' :: Char
 also fine
 However, the User's guide says "The notation `a > b` [...] indicates that the `a`
 parameter uniquely determines the `b` parameter, and might be read as “a determines b.”"
 From this I would expect that an expression like `foo 'x'` has a uniquely determined
 type, but evidently, this is not so, since it can have both type `Char` and `()`.
ex2 = foo 'x' :: ()
 not fine, with confusing error message
 Why does it expect the argument of `foo` to be of type `()` when, with
 an annotation, it accepts a `Char` argument?
 In fact, it looks like it selected the `C a a` instance and from it determined that
 it needs to solve a `C Char ()` constraint, which seems paradoxical.
 Naively I would expect GHC to talk about an ambiguous type variable, which
 is what happens if the functional dependency is removed.
ex3 = foo 'x'
{
FunDeps.hs:25:7: error:
• Couldn't match type ‘Char’ with ‘()’
arising from a functional dependency between:
constraint ‘C Char ()’ arising from a use of ‘foo’
instance ‘C a a’ at FunDeps.hs:9:1014
• In the expression: foo 'x'
In an equation for ‘ex3’: ex3 = foo 'x'

25  ex3 = foo 'x'
 ^^^^^^^
}
```
Another interesting aspect is that entering `() :: C Bool () => ()` in GHCi will produce the exact same warning twice, though I don't know if that's expected behavior:
```haskell
<interactive>:45:7: warning: [Wsimplifiableclassconstraints]
• The constraint ‘C Bool ()’ matches
instance C a ()  Defined at FunDeps.hs:15:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In an expression type signature: C Bool () => ()
In the expression: () :: C Bool () => ()
In an equation for ‘it’: it = () :: C Bool () => ()
<interactive>:45:7: warning: [Wsimplifiableclassconstraints]
• The constraint ‘C Bool ()’ matches
instance C a ()  Defined at FunDeps.hs:15:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In an expression type signature: C Bool () => ()
In the expression: () :: C Bool () => ()
In an equation for ‘it’: it = () :: C Bool () => ()
```
## Environment
* GHC version used: 8.11.0.20200127https://gitlab.haskell.org/ghc/ghc//issues/17569Why do we have both typeRep# and typeRep?20200519T12:52:49ZRichard Eisenbergrae@richarde.devWhy do we have both typeRep# and typeRep?In `Data.Typeable.Internal`, we see
```hs
class Typeable (a :: k) where
typeRep# :: TypeRep a
typeRep :: Typeable a => TypeRep a
typeRep = typeRep#
```
Why have `typeRep` separate from `typeRep#`? The only difference I can see is the specificity of the `k` variable. To wit, we have
```hs
typeRep# :: forall (k :: Type) (a :: k). Typeable @k a => TypeRep @k a
typeRep :: forall {k :: Type} (a :: k). Typeable @k a => TypeRep @k a
```
The *only* difference is the braces.
But we needn't do all this. Instead, we could define
```hs
class Typeable a where
typeRep :: TypeRep a
```
It's unfortunate not to make that explicitly polykinded, but it would be inferred to be polykinded, and `typeRep` would get the right specificity.
So, is there anything stopping us from this simplification?In `Data.Typeable.Internal`, we see
```hs
class Typeable (a :: k) where
typeRep# :: TypeRep a
typeRep :: Typeable a => TypeRep a
typeRep = typeRep#
```
Why have `typeRep` separate from `typeRep#`? The only difference I can see is the specificity of the `k` variable. To wit, we have
```hs
typeRep# :: forall (k :: Type) (a :: k). Typeable @k a => TypeRep @k a
typeRep :: forall {k :: Type} (a :: k). Typeable @k a => TypeRep @k a
```
The *only* difference is the braces.
But we needn't do all this. Instead, we could define
```hs
class Typeable a where
typeRep :: TypeRep a
```
It's unfortunate not to make that explicitly polykinded, but it would be inferred to be polykinded, and `typeRep` would get the right specificity.
So, is there anything stopping us from this simplification?https://gitlab.haskell.org/ghc/ghc//issues/17013GHC accepts DerivingViagenerated instances that violate functional dependencies20190801T11:47:52ZAlexis KingGHC accepts DerivingViagenerated instances that violate functional dependencies## Summary
Instances generated using `DerivingVia` are accepted even though equivalent handwritten instances are rejected due to violation of the (liberal) coverage condition.
## Steps to reproduce
This module demonstrates the problem:
```haskell
{# LANGUAGE DerivingVia #}
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE FlexibleInstances #}
module DerivingViaBug where
class C a b  b > a
newtype A t a = A a
instance C t (A t a)
data T = T
deriving (C a) via (A () T)
```
The above program is accepted. But if we write the `C a T` instance manually, rather than deriving it, the program is rejected:
```haskell
data T = T
instance C a T
```
```
src/DerivingViaBug.hs:13:10: error:
• Illegal instance declaration for ‘C a T’
The coverage condition fails in class ‘C’
for functional dependency: ‘b > a’
Reason: lhs type ‘T’ does not determine rhs type ‘a’
Undetermined variable: a
• In the instance declaration for ‘C a T’

13  instance C a T
 ^^^^^
```
## Expected behavior
The simplest solution to this problem would be to reject the derived instance. However, this introduces a bit of an inconsistency between functional dependencies and associated types. Consider the following similar program, which uses associated types instead of functional dependencies:
```haskell
{# LANGUAGE DerivingVia #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
module DerivingViaBug where
class C a where
type F a
newtype A t a = A a
instance C (A t a) where
type F (A t a) = t
data T = T
deriving (C) via (A () T)
```
This program is accepted, and the behavior is reasonable. The derived instance is
```haskell
instance C T where
type F T = F (A () T)
```
so `F T` is ultimately `()`. To achieve analogous behavior for functional dependencies, it seems like a reasonable derived instance could be
```haskell
instance C () T
```
which can be constructed by applying the substitution {`t` ↦ `()`, `a` ↦ `T`} to the original `C t (A t a)` instance declaration. I haven’t thought about it enough to say whether or not that would cause more problems than it would solve, however.
## Environment
* GHC version used: 8.6.5
* Operating System: macOS 10.14.5 (18F132)
* System Architecture: x86_64## Summary
Instances generated using `DerivingVia` are accepted even though equivalent handwritten instances are rejected due to violation of the (liberal) coverage condition.
## Steps to reproduce
This module demonstrates the problem:
```haskell
{# LANGUAGE DerivingVia #}
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE FlexibleInstances #}
module DerivingViaBug where
class C a b  b > a
newtype A t a = A a
instance C t (A t a)
data T = T
deriving (C a) via (A () T)
```
The above program is accepted. But if we write the `C a T` instance manually, rather than deriving it, the program is rejected:
```haskell
data T = T
instance C a T
```
```
src/DerivingViaBug.hs:13:10: error:
• Illegal instance declaration for ‘C a T’
The coverage condition fails in class ‘C’
for functional dependency: ‘b > a’
Reason: lhs type ‘T’ does not determine rhs type ‘a’
Undetermined variable: a
• In the instance declaration for ‘C a T’

13  instance C a T
 ^^^^^
```
## Expected behavior
The simplest solution to this problem would be to reject the derived instance. However, this introduces a bit of an inconsistency between functional dependencies and associated types. Consider the following similar program, which uses associated types instead of functional dependencies:
```haskell
{# LANGUAGE DerivingVia #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
module DerivingViaBug where
class C a where
type F a
newtype A t a = A a
instance C (A t a) where
type F (A t a) = t
data T = T
deriving (C) via (A () T)
```
This program is accepted, and the behavior is reasonable. The derived instance is
```haskell
instance C T where
type F T = F (A () T)
```
so `F T` is ultimately `()`. To achieve analogous behavior for functional dependencies, it seems like a reasonable derived instance could be
```haskell
instance C () T
```
which can be constructed by applying the substitution {`t` ↦ `()`, `a` ↦ `T`} to the original `C t (A t a)` instance declaration. I haven’t thought about it enough to say whether or not that would cause more problems than it would solve, however.
## Environment
* GHC version used: 8.6.5
* Operating System: macOS 10.14.5 (18F132)
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc//issues/16581Trivial Functional Dependencies (and downright nonsense) accepted20190707T18:00:07ZAnthony ClaydenTrivial Functional Dependencies (and downright nonsense) accepted# Summary
GHC accepts Functional Dependencies that are pointless and/or nonsensical.
(This ticket was originally posted as a possible 'feature'. But the allowed syntax is misleading: there's no useful behaviour. Commentary from SPJ & RAE retained below for ref.)
# Steps to reproduce
These FunDeps are accepted
class C a  a > a where  not even MultiParam
cMeth :: a > String
class D a b  a b > b where
dMeth :: a > b > String
class D2 a b  a b a b > b a b a
# Expected behavior
I expect these to be rejected, because they're pointless. The class behaves just as if there were no FunDep at all.
# Environment
* GHC version used: 8.6.4
Optional:
* Operating System: Windows
* For comparison, the validation on FunDeps in Hugs [static validation, search for "trivial"](https://github.com/FranklinChen/hugs98plusSep2006/blob/master/src/static.c) is, for each FunDep in the class decl:
* the tyvars to the right of each `>` must be nonempty;
* no tyvar can appear both left and right of the same `>`;
* no tyvar repeated left of each `>`;
* no tyvar repeated right of each `>`.
* In general, in database theory for functional dependencies, these are known as 'trivial'. (Neither the Jones 2000 paper introducing FunDeps; nor the JFP 2006 Sulzmann et al 'via CHRs paper' explicitly give these rules.)
/label ~bug
 as originally posted, for ref
# Motivation
This isn't so much a feature request as: does anybody know GHC can do this?/Is there some reasoning behind it?/I can think of a possible use.
There's a longstanding ticket #8634 which got dubbed 'Dysfunctional Dependencies'. It seems GHC already supports something like it.
# Proposal
Consider these FunDeps
class C a  a > a where  not even MultiParam
cMeth :: a > String
class D a b  a b > b where
dMeth :: a > b > String
This is accepted by GHC (8.6.4), and I can write and use instances for those classes. Those dependencies are what's called "trivial"  that is, the FunDep target also appears on LHS of the `>`. FunDep theory (such as the 'via CHRs' paper) says they shouldn't be allowed, and indeed Hugs rejects those class decls.
But wait! Here's some useful instances
instance D Int Bool where
dMeth x p = show $ if p then x else x
instance D Int Char where  rejected if FunDep is bare a > b
dMeth x y = y : show x  because FunDep conflict between instances
instance (b1 ~ Int) => D Int (b1 > b1) where
dMeth x f = show $ f x
fi = dMeth (5 :: Int) ((\x > x + x) :: Num b2 => b2 > b2)
instance {# OVERLAPPABLE #} (b ~ String) => D Int b where
dMeth x _ = "String" ++ show x
(That last instance and the `(b1 > b1)` would need `UndecidableInstances` if just FunDep `a > b`.)
OTOH I don't seem to be getting behaviour any different from just `D` without a FunDep at all. For example
f :: D a b => a > a
f x = x
is rejected as ambiguous, as would be with no FunDep on `D`.
From what I recall of 'Dysfunctional Dependencies' (by now the ticket is long and turgid), a FunDep `a b > b` does represent what's happening: for some instances you can get from `a` to `b` by the coverage conditions; for some you can get from `a` to `b` via Constraints (and `UndecidableInstances`); for some you need to also look at the combo of `a, b`  in that case, the Wanted from the use site will give sufficient typing to select the instance and then fix `b`. Just trust me that when the FunDep says `... > b` you'll be able to infer `b`.# Summary
GHC accepts Functional Dependencies that are pointless and/or nonsensical.
(This ticket was originally posted as a possible 'feature'. But the allowed syntax is misleading: there's no useful behaviour. Commentary from SPJ & RAE retained below for ref.)
# Steps to reproduce
These FunDeps are accepted
class C a  a > a where  not even MultiParam
cMeth :: a > String
class D a b  a b > b where
dMeth :: a > b > String
class D2 a b  a b a b > b a b a
# Expected behavior
I expect these to be rejected, because they're pointless. The class behaves just as if there were no FunDep at all.
# Environment
* GHC version used: 8.6.4
Optional:
* Operating System: Windows
* For comparison, the validation on FunDeps in Hugs [static validation, search for "trivial"](https://github.com/FranklinChen/hugs98plusSep2006/blob/master/src/static.c) is, for each FunDep in the class decl:
* the tyvars to the right of each `>` must be nonempty;
* no tyvar can appear both left and right of the same `>`;
* no tyvar repeated left of each `>`;
* no tyvar repeated right of each `>`.
* In general, in database theory for functional dependencies, these are known as 'trivial'. (Neither the Jones 2000 paper introducing FunDeps; nor the JFP 2006 Sulzmann et al 'via CHRs paper' explicitly give these rules.)
/label ~bug
 as originally posted, for ref
# Motivation
This isn't so much a feature request as: does anybody know GHC can do this?/Is there some reasoning behind it?/I can think of a possible use.
There's a longstanding ticket #8634 which got dubbed 'Dysfunctional Dependencies'. It seems GHC already supports something like it.
# Proposal
Consider these FunDeps
class C a  a > a where  not even MultiParam
cMeth :: a > String
class D a b  a b > b where
dMeth :: a > b > String
This is accepted by GHC (8.6.4), and I can write and use instances for those classes. Those dependencies are what's called "trivial"  that is, the FunDep target also appears on LHS of the `>`. FunDep theory (such as the 'via CHRs' paper) says they shouldn't be allowed, and indeed Hugs rejects those class decls.
But wait! Here's some useful instances
instance D Int Bool where
dMeth x p = show $ if p then x else x
instance D Int Char where  rejected if FunDep is bare a > b
dMeth x y = y : show x  because FunDep conflict between instances
instance (b1 ~ Int) => D Int (b1 > b1) where
dMeth x f = show $ f x
fi = dMeth (5 :: Int) ((\x > x + x) :: Num b2 => b2 > b2)
instance {# OVERLAPPABLE #} (b ~ String) => D Int b where
dMeth x _ = "String" ++ show x
(That last instance and the `(b1 > b1)` would need `UndecidableInstances` if just FunDep `a > b`.)
OTOH I don't seem to be getting behaviour any different from just `D` without a FunDep at all. For example
f :: D a b => a > a
f x = x
is rejected as ambiguous, as would be with no FunDep on `D`.
From what I recall of 'Dysfunctional Dependencies' (by now the ticket is long and turgid), a FunDep `a b > b` does represent what's happening: for some instances you can get from `a` to `b` by the coverage conditions; for some you can get from `a` to `b` via Constraints (and `UndecidableInstances`); for some you need to also look at the combo of `a, b`  in that case, the Wanted from the use site will give sufficient typing to select the instance and then fix `b`. Just trust me that when the FunDep says `... > b` you'll be able to infer `b`.https://gitlab.haskell.org/ghc/ghc//issues/16430System FC for FunDeps: not doing what it says on the tin20190323T11:39:36ZAnthony ClaydenSystem FC for FunDeps: not doing what it says on the tinConsider this example from the 2011 paper 'System F with Type Equality Coercions', section 2.3 discussing FunDeps
class F a b  a > b
instance F Int Bool
class D a where { op :: F a b => a > b }
instance D Int where { op _ = True }
The paper says
> Using FC, this problem [of typing the definition of `op` in the instance `D Int`] is easily solved: the coercion in the dictionary for `F` enables the result of `op` to be cast to type `b` as required.
I get (I'm at GHC 8.6.1, on a Windows machine)
* Couldn't match expected type `b' with actual type `Bool'
`b' is a rigid type variable bound by
the type signature for:
op :: forall b. F Int b => Int > b
* In the expression: True
In an equation for `op': op _ = True
In the instance declaration for `D Int'
* Relevant bindings include
op :: Int > b
(I have a reallife example where I bumped into this rejection.)Consider this example from the 2011 paper 'System F with Type Equality Coercions', section 2.3 discussing FunDeps
class F a b  a > b
instance F Int Bool
class D a where { op :: F a b => a > b }
instance D Int where { op _ = True }
The paper says
> Using FC, this problem [of typing the definition of `op` in the instance `D Int`] is easily solved: the coercion in the dictionary for `F` enables the result of `op` to be cast to type `b` as required.
I get (I'm at GHC 8.6.1, on a Windows machine)
* Couldn't match expected type `b' with actual type `Bool'
`b' is a rigid type variable bound by
the type signature for:
op :: forall b. F Int b => Int > b
* In the expression: True
In an equation for `op': op _ = True
In the instance declaration for `D Int'
* Relevant bindings include
op :: Int > b
(I have a reallife example where I bumped into this rejection.)https://gitlab.haskell.org/ghc/ghc//issues/15927Weird interaction between fundeps and overlappable instances20190707T18:02:24ZDarwin226Weird interaction between fundeps and overlappable instancesConsider this code
```hs
class MyState s m  m > s where
getMyState :: m s
instance {# OVERLAPPABLE #} (MyState s m, MonadTrans t, Monad m) => MyState s (t m) where
getMyState = lift getMyState
instance Monad m => MyState s (StateT s m) where
getMyState = get
f :: (MyState Int m, MyState Char m, MonadIO m) => m ()
f = do
int < getMyState
str < getMyState
liftIO $ putStrLn (replicate int str)
works1 :: (MyState s m, Show s, MonadIO m) => m ()
works1 = do
a < getMyState
liftIO (print a)
works2 = runStateT (runStateT f (5 :: Int)) 'a'
```
It defines a class similar to `MonadState` of mtl. There is a functional dependency in place, just like with `MonadState` and we can see that it works the same because `works1` compiles where `a` would have an ambiguous type otherwise.
The `f` function "shouldn't" compile because it's using two different states at once subverting the functional dependency restriction. It does however compile because an explicit type signature is provided with an unsolvable constraint.
Now the really weird part is that `works2` also compiles and produces the expected result even though it's using `f`.
Here's what I think is happening: instance resolution is looking for `MyState Int (StateT Char m)` and it finds the `MyState s (StateT s m)` instance. Instead of complaining that `Int` doesn't match `Char` (due to the fundep), it just rejects the instance and takes the overlappable one that does match. In the case where the state is unknown (i.e. both instances match), the fundep kicks in. That's why `runStateT works1 True` works.
Is this intended behavior? It seems pretty useful in some situations and I've tested this with 8.2 and 8.6 with the same results.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.2 
 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":"Weird interaction between fundeps and overlappable instances","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this code\r\n\r\n{{{#!hs\r\nclass MyState s m  m > s where\r\n getMyState :: m s\r\ninstance {# OVERLAPPABLE #} (MyState s m, MonadTrans t, Monad m) => MyState s (t m) where\r\n getMyState = lift getMyState\r\ninstance Monad m => MyState s (StateT s m) where\r\n getMyState = get\r\n\r\nf :: (MyState Int m, MyState Char m, MonadIO m) => m ()\r\nf = do\r\n int < getMyState\r\n str < getMyState\r\n liftIO $ putStrLn (replicate int str)\r\n\r\n\r\nworks1 :: (MyState s m, Show s, MonadIO m) => m ()\r\nworks1 = do\r\n a < getMyState\r\n liftIO (print a)\r\n\r\nworks2 = runStateT (runStateT f (5 :: Int)) 'a'\r\n}}}\r\n\r\nIt defines a class similar to `MonadState` of mtl. There is a functional dependency in place, just like with `MonadState` and we can see that it works the same because `works1` compiles where `a` would have an ambiguous type otherwise.\r\n\r\nThe `f` function \"shouldn't\" compile because it's using two different states at once subverting the functional dependency restriction. It does however compile because an explicit type signature is provided with an unsolvable constraint. \r\n\r\nNow the really weird part is that `works2` also compiles and produces the expected result even though it's using `f`.\r\n\r\nHere's what I think is happening: instance resolution is looking for `MyState Int (StateT Char m)` and it finds the `MyState s (StateT s m)` instance. Instead of complaining that `Int` doesn't match `Char` (due to the fundep), it just rejects the instance and takes the overlappable one that does match. In the case where the state is unknown (i.e. both instances match), the fundep kicks in. That's why `runStateT works1 True` works.\r\n\r\nIs this intended behavior? It seems pretty useful in some situations and I've tested this with 8.2 and 8.6 with the same results.","type_of_failure":"OtherFailure","blocking":[]} >Consider this code
```hs
class MyState s m  m > s where
getMyState :: m s
instance {# OVERLAPPABLE #} (MyState s m, MonadTrans t, Monad m) => MyState s (t m) where
getMyState = lift getMyState
instance Monad m => MyState s (StateT s m) where
getMyState = get
f :: (MyState Int m, MyState Char m, MonadIO m) => m ()
f = do
int < getMyState
str < getMyState
liftIO $ putStrLn (replicate int str)
works1 :: (MyState s m, Show s, MonadIO m) => m ()
works1 = do
a < getMyState
liftIO (print a)
works2 = runStateT (runStateT f (5 :: Int)) 'a'
```
It defines a class similar to `MonadState` of mtl. There is a functional dependency in place, just like with `MonadState` and we can see that it works the same because `works1` compiles where `a` would have an ambiguous type otherwise.
The `f` function "shouldn't" compile because it's using two different states at once subverting the functional dependency restriction. It does however compile because an explicit type signature is provided with an unsolvable constraint.
Now the really weird part is that `works2` also compiles and produces the expected result even though it's using `f`.
Here's what I think is happening: instance resolution is looking for `MyState Int (StateT Char m)` and it finds the `MyState s (StateT s m)` instance. Instead of complaining that `Int` doesn't match `Char` (due to the fundep), it just rejects the instance and takes the overlappable one that does match. In the case where the state is unknown (i.e. both instances match), the fundep kicks in. That's why `runStateT works1 True` works.
Is this intended behavior? It seems pretty useful in some situations and I've tested this with 8.2 and 8.6 with the same results.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.2 
 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":"Weird interaction between fundeps and overlappable instances","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this code\r\n\r\n{{{#!hs\r\nclass MyState s m  m > s where\r\n getMyState :: m s\r\ninstance {# OVERLAPPABLE #} (MyState s m, MonadTrans t, Monad m) => MyState s (t m) where\r\n getMyState = lift getMyState\r\ninstance Monad m => MyState s (StateT s m) where\r\n getMyState = get\r\n\r\nf :: (MyState Int m, MyState Char m, MonadIO m) => m ()\r\nf = do\r\n int < getMyState\r\n str < getMyState\r\n liftIO $ putStrLn (replicate int str)\r\n\r\n\r\nworks1 :: (MyState s m, Show s, MonadIO m) => m ()\r\nworks1 = do\r\n a < getMyState\r\n liftIO (print a)\r\n\r\nworks2 = runStateT (runStateT f (5 :: Int)) 'a'\r\n}}}\r\n\r\nIt defines a class similar to `MonadState` of mtl. There is a functional dependency in place, just like with `MonadState` and we can see that it works the same because `works1` compiles where `a` would have an ambiguous type otherwise.\r\n\r\nThe `f` function \"shouldn't\" compile because it's using two different states at once subverting the functional dependency restriction. It does however compile because an explicit type signature is provided with an unsolvable constraint. \r\n\r\nNow the really weird part is that `works2` also compiles and produces the expected result even though it's using `f`.\r\n\r\nHere's what I think is happening: instance resolution is looking for `MyState Int (StateT Char m)` and it finds the `MyState s (StateT s m)` instance. Instead of complaining that `Int` doesn't match `Char` (due to the fundep), it just rejects the instance and takes the overlappable one that does match. In the case where the state is unknown (i.e. both instances match), the fundep kicks in. That's why `runStateT works1 True` works.\r\n\r\nIs this intended behavior? It seems pretty useful in some situations and I've tested this with 8.2 and 8.6 with the same results.","type_of_failure":"OtherFailure","blocking":[]} >8.6.3https://gitlab.haskell.org/ghc/ghc//issues/15632Undependable Dependencies20200310T02:42:13ZAntCUndependable DependenciesConsider
```hs
{# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
GADTs, FlexibleInstances, FlexibleContexts,
UndecidableInstances #}
data Hither = Hither deriving (Eq, Show, Read)  just three
data Thither = Thither deriving (Eq, Show, Read)  distinct
data Yon = Yon deriving (Eq, Show, Read)  types
class Whither a b  a > b where
whither :: a > b > b
 instance Whither Int Hither where  rejected: FunDep conflict
 whither _ y = y  with Thither instance, so
instance {# OVERLAPPING #} (b ~ Hither) => Whither Int b where
whither _ y = y
instance {# OVERLAPS #} Whither a Thither where
whither _ y = y
instance {# OVERLAPPABLE #} (b ~ Yon) => Whither a b where
whither _ y = y
f :: Whither Int b => Int > b > b
f = whither
g :: Whither Bool b => Bool > b > b
g = whither
```
Should those three instances be accepted together? In particular, the published work on FDs (including the FDs through CHRs paper) says the `Thither` instance should behave as if:
```hs
instance (beta ~ Thither) => Whither a beta where ...
```
(in which `beta` is a unification variable and the `~` constraint is type improvement under the FD.) But now the instance head is the same as the `Yon` instance, modulo alpha renaming; with the constraints being contrary.
That's demonstrated by the inferred/improved type for `g`:
```hs
*Whither> :t g
===> g :: Bool > Thither > Thither  and yet
*Whither> g True Yon
===> Yon
```
What do I expect here?
 At least the `Thither` and `Yon` instances to be rejected as inconsistent under the FunDep.
 (The `Hither` instance is also inconsistent, going by the strict interpretation in published work. But GHC's rule here is bogus, as documented in Trac #10675.)
Exploiting Overlapping instances is essential to making this go wrong. The published work shies away from considering `FunDeps + Overlap`; and yet specifying the semantics as if the instances used bare unification variables is almost inevitably going give overlaps  especially if there are multiple FDs.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1beta1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #10675 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Undependable Dependencies","status":"New","operating_system":"","component":"Compiler","related":[10675],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1beta1","keywords":["FunctionalDependencies,","OverlappingInstances"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider\r\n\r\n{{{#!hs\r\n{# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,\r\n GADTs, FlexibleInstances, FlexibleContexts,\r\n UndecidableInstances #}\r\n\r\n\r\ndata Hither = Hither deriving (Eq, Show, Read)\t\t just three\r\ndata Thither = Thither deriving (Eq, Show, Read)\t distinct\r\ndata Yon = Yon deriving (Eq, Show, Read)\t\t types\r\n\r\nclass Whither a b  a > b where\r\n whither :: a > b > b\r\n\r\n instance Whither Int Hither where\t rejected: FunDep conflict\r\n whither _ y = y\t\t\t with Thither instance, so\r\n\r\ninstance {# OVERLAPPING #} (b ~ Hither) => Whither Int b where\r\n whither _ y = y\r\n\r\ninstance {# OVERLAPS #} Whither a Thither where\r\n whither _ y = y\r\ninstance {# OVERLAPPABLE #} (b ~ Yon) => Whither a b where\r\n whither _ y = y\r\n\r\nf :: Whither Int b => Int > b > b\r\nf = whither\r\n\r\ng :: Whither Bool b => Bool > b > b\r\ng = whither\r\n}}}\r\n\r\nShould those three instances be accepted together? In particular, the published work on FDs (including the FDs through CHRs paper) says the `Thither` instance should behave as if:\r\n\r\n{{{#!hs\r\ninstance (beta ~ Thither) => Whither a beta where ...\r\n}}}\r\n(in which `beta` is a unification variable and the `~` constraint is type improvement under the FD.) But now the instance head is the same as the `Yon` instance, modulo alpha renaming; with the constraints being contrary.\r\n\r\nThat's demonstrated by the inferred/improved type for `g`:\r\n\r\n{{{#!hs\r\n*Whither> :t g\r\n===> g :: Bool > Thither > Thither  and yet\r\n\r\n*Whither> g True Yon\r\n===> Yon\r\n}}}\r\n\r\nWhat do I expect here?\r\n* At least the `Thither` and `Yon` instances to be rejected as inconsistent under the FunDep.\r\n* (The `Hither` instance is also inconsistent, going by the strict interpretation in published work. But GHC's rule here is bogus, as documented in Trac #10675.)\r\n\r\nExploiting Overlapping instances is essential to making this go wrong. The published work shies away from considering `FunDeps + Overlap`; and yet specifying the semantics as if the instances used bare unification variables is almost inevitably going give overlaps  especially if there are multiple FDs.","type_of_failure":"OtherFailure","blocking":[]} >Consider
```hs
{# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
GADTs, FlexibleInstances, FlexibleContexts,
UndecidableInstances #}
data Hither = Hither deriving (Eq, Show, Read)  just three
data Thither = Thither deriving (Eq, Show, Read)  distinct
data Yon = Yon deriving (Eq, Show, Read)  types
class Whither a b  a > b where
whither :: a > b > b
 instance Whither Int Hither where  rejected: FunDep conflict
 whither _ y = y  with Thither instance, so
instance {# OVERLAPPING #} (b ~ Hither) => Whither Int b where
whither _ y = y
instance {# OVERLAPS #} Whither a Thither where
whither _ y = y
instance {# OVERLAPPABLE #} (b ~ Yon) => Whither a b where
whither _ y = y
f :: Whither Int b => Int > b > b
f = whither
g :: Whither Bool b => Bool > b > b
g = whither
```
Should those three instances be accepted together? In particular, the published work on FDs (including the FDs through CHRs paper) says the `Thither` instance should behave as if:
```hs
instance (beta ~ Thither) => Whither a beta where ...
```
(in which `beta` is a unification variable and the `~` constraint is type improvement under the FD.) But now the instance head is the same as the `Yon` instance, modulo alpha renaming; with the constraints being contrary.
That's demonstrated by the inferred/improved type for `g`:
```hs
*Whither> :t g
===> g :: Bool > Thither > Thither  and yet
*Whither> g True Yon
===> Yon
```
What do I expect here?
 At least the `Thither` and `Yon` instances to be rejected as inconsistent under the FunDep.
 (The `Hither` instance is also inconsistent, going by the strict interpretation in published work. But GHC's rule here is bogus, as documented in Trac #10675.)
Exploiting Overlapping instances is essential to making this go wrong. The published work shies away from considering `FunDeps + Overlap`; and yet specifying the semantics as if the instances used bare unification variables is almost inevitably going give overlaps  especially if there are multiple FDs.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1beta1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #10675 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Undependable Dependencies","status":"New","operating_system":"","component":"Compiler","related":[10675],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1beta1","keywords":["FunctionalDependencies,","OverlappingInstances"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider\r\n\r\n{{{#!hs\r\n{# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,\r\n GADTs, FlexibleInstances, FlexibleContexts,\r\n UndecidableInstances #}\r\n\r\n\r\ndata Hither = Hither deriving (Eq, Show, Read)\t\t just three\r\ndata Thither = Thither deriving (Eq, Show, Read)\t distinct\r\ndata Yon = Yon deriving (Eq, Show, Read)\t\t types\r\n\r\nclass Whither a b  a > b where\r\n whither :: a > b > b\r\n\r\n instance Whither Int Hither where\t rejected: FunDep conflict\r\n whither _ y = y\t\t\t with Thither instance, so\r\n\r\ninstance {# OVERLAPPING #} (b ~ Hither) => Whither Int b where\r\n whither _ y = y\r\n\r\ninstance {# OVERLAPS #} Whither a Thither where\r\n whither _ y = y\r\ninstance {# OVERLAPPABLE #} (b ~ Yon) => Whither a b where\r\n whither _ y = y\r\n\r\nf :: Whither Int b => Int > b > b\r\nf = whither\r\n\r\ng :: Whither Bool b => Bool > b > b\r\ng = whither\r\n}}}\r\n\r\nShould those three instances be accepted together? In particular, the published work on FDs (including the FDs through CHRs paper) says the `Thither` instance should behave as if:\r\n\r\n{{{#!hs\r\ninstance (beta ~ Thither) => Whither a beta where ...\r\n}}}\r\n(in which `beta` is a unification variable and the `~` constraint is type improvement under the FD.) But now the instance head is the same as the `Yon` instance, modulo alpha renaming; with the constraints being contrary.\r\n\r\nThat's demonstrated by the inferred/improved type for `g`:\r\n\r\n{{{#!hs\r\n*Whither> :t g\r\n===> g :: Bool > Thither > Thither  and yet\r\n\r\n*Whither> g True Yon\r\n===> Yon\r\n}}}\r\n\r\nWhat do I expect here?\r\n* At least the `Thither` and `Yon` instances to be rejected as inconsistent under the FunDep.\r\n* (The `Hither` instance is also inconsistent, going by the strict interpretation in published work. But GHC's rule here is bogus, as documented in Trac #10675.)\r\n\r\nExploiting Overlapping instances is essential to making this go wrong. The published work shies away from considering `FunDeps + Overlap`; and yet specifying the semantics as if the instances used bare unification variables is almost inevitably going give overlaps  especially if there are multiple FDs.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/14778FunDep origin not correctly attributed20190707T18:15:39ZSimon Peyton JonesFunDep origin not correctly attributedIn `TcInteract.improveTopFunEqs` we do not give the derived constraints an origin of `FunDepOrigin`. As a result, `dropDerivedSimples` will discard even an insoluble constraint arising from a fundep. In contrast class instance fundeps do have `FunDepOrigin` and are kept.
This is at least inconsistent. And we get less good error messages.
Shows up in tests `T13651, `TR8450`, `T13506`, `T14325\`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 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":"FunDep origin not correctly attributed","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["FunDeps"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In `TcInteract.improveTopFunEqs` we do not give the derived constraints an origin of `FunDepOrigin`. As a result, `dropDerivedSimples` will discard even an insoluble constraint arising from a fundep. In contrast class instance fundeps do have `FunDepOrigin` and are kept.\r\n\r\nThis is at least inconsistent. And we get less good error messages.\r\n\r\nShows up in tests `T13651, `TR8450`, `T13506`, `T14325`.","type_of_failure":"OtherFailure","blocking":[]} >In `TcInteract.improveTopFunEqs` we do not give the derived constraints an origin of `FunDepOrigin`. As a result, `dropDerivedSimples` will discard even an insoluble constraint arising from a fundep. In contrast class instance fundeps do have `FunDepOrigin` and are kept.
This is at least inconsistent. And we get less good error messages.
Shows up in tests `T13651, `TR8450`, `T13506`, `T14325\`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 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":"FunDep origin not correctly attributed","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["FunDeps"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In `TcInteract.improveTopFunEqs` we do not give the derived constraints an origin of `FunDepOrigin`. As a result, `dropDerivedSimples` will discard even an insoluble constraint arising from a fundep. In contrast class instance fundeps do have `FunDepOrigin` and are kept.\r\n\r\nThis is at least inconsistent. And we get less good error messages.\r\n\r\nShows up in tests `T13651, `TR8450`, `T13506`, `T14325`.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14745Functional dependency conflicts in givens20190707T18:15:47ZSimon Peyton JonesFunctional dependency conflicts in givensConsider this
```
{# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies #}
module FunDep where
class C a b c  a > b c
instance C Int Bool Char
f :: (C Int b c) => a > c
f = undefined
```
When doing the ambiguity check we effectively ask whether this would typecheck
```
g :: (C Int b c) => a > c
g = f
```
We instantiate `f`'s type, and try to solve from `g`'s type signature. So we end up with
```
[G] d1: C Int b c
[W] d2: C Int beta c
```
Now, from the fundeps we get
```
Interact d1 with the instance:
[D] b ~ Bool, [D] c ~ Char
Ineract d2 with the instance:
[D] beta ~ Bool, [D] c ~ Char
Interact d1 with d2
[D] beta ~ b
```
What is annoying is that if we unify `beta := b`, we can solve the
\[W\] constraint from \[G\], leaving only \[D\] constraints which we don't
even always report (see discussion on #12466). But if, randomly,
we instead unify `beta := Bool`, we get an insoluble constraint
`[W] C Int Bool c`, which we report. So whether or not typechecking
succeeds is rather random; very unsatisfactory.
What is really wrong? Well, that Given constraint `(C Int b c)` is in
conflict with the toplevel instance decl. Maybe we should fail
if that happens? But see #12466... and `Note [Given errors]` in `TcErrors`.
The test program in Trac #13651 is just like this, only with type functions rather than type classes.
I'm not sure what to do, but I'm leaving this ticket as a record that
all is not well.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 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":"Functional dependency conflicts in givens","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this\r\n{{{\r\n{# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies #}\r\nmodule FunDep where\r\n\r\n class C a b c  a > b c\r\n\r\n instance C Int Bool Char\r\n\r\n f :: (C Int b c) => a > c\r\n f = undefined\r\n}}}\r\nWhen doing the ambiguity check we effectively ask whether this would typecheck\r\n{{{\r\n g :: (C Int b c) => a > c\r\n g = f\r\n}}}\r\nWe instantiate `f`'s type, and try to solve from `g`'s type signature. So we end up with\r\n{{{\r\n [G] d1: C Int b c\r\n [W] d2: C Int beta c\r\n}}}\r\nNow, from the fundeps we get\r\n{{{\r\nInteract d1 with the instance:\r\n [D] b ~ Bool, [D] c ~ Char\r\n\r\nIneract d2 with the instance:\r\n [D] beta ~ Bool, [D] c ~ Char\r\n\r\nInteract d1 with d2\r\n [D] beta ~ b\r\n}}}\r\nWhat is annoying is that if we unify `beta := b`, we can solve the\r\n[W] constraint from [G], leaving only [D] constraints which we don't\r\neven always report (see discussion on #12466). But if, randomly,\r\nwe instead unify `beta := Bool`, we get an insoluble constraint\r\n`[W] C Int Bool c`, which we report. So whether or not typechecking\r\nsucceeds is rather random; very unsatisfactory.\r\n\r\nWhat is really wrong? Well, that Given constraint `(C Int b c)` is in\r\nconflict with the toplevel instance decl. Maybe we should fail\r\nif that happens? But see #12466... and `Note [Given errors]` in `TcErrors`.\r\n\r\nThe test program in Trac #13651 is just like this, only with type functions rather than type classes.\r\n\r\nI'm not sure what to do, but I'm leaving this ticket as a record that\r\nall is not well.\r\n","type_of_failure":"OtherFailure","blocking":[]} >Consider this
```
{# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies #}
module FunDep where
class C a b c  a > b c
instance C Int Bool Char
f :: (C Int b c) => a > c
f = undefined
```
When doing the ambiguity check we effectively ask whether this would typecheck
```
g :: (C Int b c) => a > c
g = f
```
We instantiate `f`'s type, and try to solve from `g`'s type signature. So we end up with
```
[G] d1: C Int b c
[W] d2: C Int beta c
```
Now, from the fundeps we get
```
Interact d1 with the instance:
[D] b ~ Bool, [D] c ~ Char
Ineract d2 with the instance:
[D] beta ~ Bool, [D] c ~ Char
Interact d1 with d2
[D] beta ~ b
```
What is annoying is that if we unify `beta := b`, we can solve the
\[W\] constraint from \[G\], leaving only \[D\] constraints which we don't
even always report (see discussion on #12466). But if, randomly,
we instead unify `beta := Bool`, we get an insoluble constraint
`[W] C Int Bool c`, which we report. So whether or not typechecking
succeeds is rather random; very unsatisfactory.
What is really wrong? Well, that Given constraint `(C Int b c)` is in
conflict with the toplevel instance decl. Maybe we should fail
if that happens? But see #12466... and `Note [Given errors]` in `TcErrors`.
The test program in Trac #13651 is just like this, only with type functions rather than type classes.
I'm not sure what to do, but I'm leaving this ticket as a record that
all is not well.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 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":"Functional dependency conflicts in givens","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this\r\n{{{\r\n{# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies #}\r\nmodule FunDep where\r\n\r\n class C a b c  a > b c\r\n\r\n instance C Int Bool Char\r\n\r\n f :: (C Int b c) => a > c\r\n f = undefined\r\n}}}\r\nWhen doing the ambiguity check we effectively ask whether this would typecheck\r\n{{{\r\n g :: (C Int b c) => a > c\r\n g = f\r\n}}}\r\nWe instantiate `f`'s type, and try to solve from `g`'s type signature. So we end up with\r\n{{{\r\n [G] d1: C Int b c\r\n [W] d2: C Int beta c\r\n}}}\r\nNow, from the fundeps we get\r\n{{{\r\nInteract d1 with the instance:\r\n [D] b ~ Bool, [D] c ~ Char\r\n\r\nIneract d2 with the instance:\r\n [D] beta ~ Bool, [D] c ~ Char\r\n\r\nInteract d1 with d2\r\n [D] beta ~ b\r\n}}}\r\nWhat is annoying is that if we unify `beta := b`, we can solve the\r\n[W] constraint from [G], leaving only [D] constraints which we don't\r\neven always report (see discussion on #12466). But if, randomly,\r\nwe instead unify `beta := Bool`, we get an insoluble constraint\r\n`[W] C Int Bool c`, which we report. So whether or not typechecking\r\nsucceeds is rather random; very unsatisfactory.\r\n\r\nWhat is really wrong? Well, that Given constraint `(C Int b c)` is in\r\nconflict with the toplevel instance decl. Maybe we should fail\r\nif that happens? But see #12466... and `Note [Given errors]` in `TcErrors`.\r\n\r\nThe test program in Trac #13651 is just like this, only with type functions rather than type classes.\r\n\r\nI'm not sure what to do, but I'm leaving this ticket as a record that\r\nall is not well.\r\n","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/12860GeneralizedNewtypeDeriving + MultiParamTypeClasses sends typechecker into an ...20190801T11:47:53ZRyan ScottGeneralizedNewtypeDeriving + MultiParamTypeClasses sends typechecker into an infinite loopThis worked in GHC 7.6.3, but ever since GHC 7.8, this code will cause the typechecker to loop infinitely:
```hs
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE GeneralizedNewtypeDeriving #}
{# LANGUAGE MultiParamTypeClasses #}
module Bug where
class C a b  a > b where
c :: a > Int
newtype Foo a = Foo a
deriving (C b)
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GeneralizedNewtypeDeriving + MultiParamTypeClasses sends typechecker into an infinite loop","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This worked in GHC 7.6.3, but ever since GHC 7.8, this code will cause the typechecker to loop infinitely:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FunctionalDependencies #}\r\n{# LANGUAGE GeneralizedNewtypeDeriving #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\nmodule Bug where\r\n\r\nclass C a b  a > b where\r\n c :: a > Int\r\n\r\nnewtype Foo a = Foo a\r\n deriving (C b)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >This worked in GHC 7.6.3, but ever since GHC 7.8, this code will cause the typechecker to loop infinitely:
```hs
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE GeneralizedNewtypeDeriving #}
{# LANGUAGE MultiParamTypeClasses #}
module Bug where
class C a b  a > b where
c :: a > Int
newtype Foo a = Foo a
deriving (C b)
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GeneralizedNewtypeDeriving + MultiParamTypeClasses sends typechecker into an infinite loop","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This worked in GHC 7.6.3, but ever since GHC 7.8, this code will cause the typechecker to loop infinitely:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FunctionalDependencies #}\r\n{# LANGUAGE GeneralizedNewtypeDeriving #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\nmodule Bug where\r\n\r\nclass C a b  a > b where\r\n c :: a > Int\r\n\r\nnewtype Foo a = Foo a\r\n deriving (C b)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/12704Check if constraint synonym satisfies functional dependencies20190707T18:25:29ZEdward Z. YangCheck if constraint synonym satisfies functional dependenciesWhen we resolve #12679, it will be possible to implement an abstract type class using a constraint synonym. However, in my implementation, I didn't implement functional dependency checking:
```
signature H where
class F a b  a > b
 This should be an invalid implementation
module H where
type F a b = (Eq a, Eq b)
```
The check is annoying fiddly: we have to descend into the constraint synonym, collect all the implied fundeps, and then see if we have the ones we need, so I didn't implement it. Maybe some time.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  low 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Check if constraint synonym satisfies functional dependencies","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When we resolve #12679, it will be possible to implement an abstract type class using a constraint synonym. However, in my implementation, I didn't implement functional dependency checking:\r\n\r\n{{{\r\nsignature H where\r\n class F a b  a > b\r\n\r\n This should be an invalid implementation\r\nmodule H where\r\n type F a b = (Eq a, Eq b)\r\n}}}\r\n\r\nThe check is annoying fiddly: we have to descend into the constraint synonym, collect all the implied fundeps, and then see if we have the ones we need, so I didn't implement it. Maybe some time.","type_of_failure":"OtherFailure","blocking":[]} >When we resolve #12679, it will be possible to implement an abstract type class using a constraint synonym. However, in my implementation, I didn't implement functional dependency checking:
```
signature H where
class F a b  a > b
 This should be an invalid implementation
module H where
type F a b = (Eq a, Eq b)
```
The check is annoying fiddly: we have to descend into the constraint synonym, collect all the implied fundeps, and then see if we have the ones we need, so I didn't implement it. Maybe some time.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  low 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Check if constraint synonym satisfies functional dependencies","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When we resolve #12679, it will be possible to implement an abstract type class using a constraint synonym. However, in my implementation, I didn't implement functional dependency checking:\r\n\r\n{{{\r\nsignature H where\r\n class F a b  a > b\r\n\r\n This should be an invalid implementation\r\nmodule H where\r\n type F a b = (Eq a, Eq b)\r\n}}}\r\n\r\nThe check is annoying fiddly: we have to descend into the constraint synonym, collect all the implied fundeps, and then see if we have the ones we need, so I didn't implement it. Maybe some time.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/12647Can't capture improvement of functional dependencies20190707T18:25:42ZIcelandjackCan't capture improvement of functional dependencies[Type Families with Class, Type Classes with Family](http://www.diku.dk/~paba/pubs/files/serrano15haskellpaper.pdf) discusses [instance improvement](https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025d9da2a70#pdfinstanceimprovement) with the example
```hs
class Collection c e  c > e where
empty :: c
add :: e > c > c
instance Collection [a] a where
empty :: [a]
empty = []
add :: a > [a] > [a]
add = (:)
```
I wondered how to express that `x ~ Int` can be deduced from `Collection [Int] x` using improvement, I first attempted using the [constraints](https://hackage.haskell.org/package/constraints) machinery:
```hs
data Dict c where
Dict :: c => Dict c
newtype a : b = Sub (a => Dict b)
```
but I'm not able to construct a term of type `Collection [Int] x : (Int ~ x)` proving that `Collection [Int] x` entails `Int ~ x`:
```
ghci> Sub Dict :: Collection [Int] x : (Int ~ x)
<interactive>:52:5: error:
• Couldn't match type ‘x1’ with ‘Int’ arising from a use of ‘Dict’
‘x1’ is a rigid type variable bound by
an expression type signature:
forall x1. Collection [Int] x1 : Int ~ x1
at <interactive>:52:13
• In the first argument of ‘Sub’, namely ‘Dict’
In the expression: Sub Dict :: Collection [Int] x : (Int ~ x)
In an equation for ‘it’:
it = Sub Dict :: Collection [Int] x : (Int ~ x)
```
Is this due to overlapping instances or something?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  None 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Can't capture improvement of functional dependencies","status":"New","operating_system":"","component":"None","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["FunctionalDependencies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"[http://www.diku.dk/~paba/pubs/files/serrano15haskellpaper.pdf Type Families with Class, Type Classes with Family] discusses [https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025d9da2a70#pdfinstanceimprovement instance improvement] with the example\r\n\r\n{{{#!hs\r\nclass Collection c e  c > e where\r\n empty :: c\r\n add :: e > c > c\r\n\r\ninstance Collection [a] a where\r\n empty :: [a]\r\n empty = []\r\n\r\n add :: a > [a] > [a]\r\n add = (:)\r\n}}}\r\n\r\nI wondered how to express that `x ~ Int` can be deduced from `Collection [Int] x` using improvement, I first attempted using the [https://hackage.haskell.org/package/constraints constraints] machinery:\r\n\r\n{{{#!hs\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\nnewtype a : b = Sub (a => Dict b)\r\n}}}\r\n\r\nbut I'm not able to construct a term of type `Collection [Int] x : (Int ~ x)` proving that `Collection [Int] x` entails `Int ~ x`:\r\n\r\n{{{\r\nghci> Sub Dict :: Collection [Int] x : (Int ~ x)\r\n\r\n<interactive>:52:5: error:\r\n • Couldn't match type ‘x1’ with ‘Int’ arising from a use of ‘Dict’\r\n ‘x1’ is a rigid type variable bound by\r\n an expression type signature:\r\n forall x1. Collection [Int] x1 : Int ~ x1\r\n at <interactive>:52:13\r\n • In the first argument of ‘Sub’, namely ‘Dict’\r\n In the expression: Sub Dict :: Collection [Int] x : (Int ~ x)\r\n In an equation for ‘it’:\r\n it = Sub Dict :: Collection [Int] x : (Int ~ x)\r\n}}}\r\n\r\nIs this due to overlapping instances or something?","type_of_failure":"OtherFailure","blocking":[]} >[Type Families with Class, Type Classes with Family](http://www.diku.dk/~paba/pubs/files/serrano15haskellpaper.pdf) discusses [instance improvement](https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025d9da2a70#pdfinstanceimprovement) with the example
```hs
class Collection c e  c > e where
empty :: c
add :: e > c > c
instance Collection [a] a where
empty :: [a]
empty = []
add :: a > [a] > [a]
add = (:)
```
I wondered how to express that `x ~ Int` can be deduced from `Collection [Int] x` using improvement, I first attempted using the [constraints](https://hackage.haskell.org/package/constraints) machinery:
```hs
data Dict c where
Dict :: c => Dict c
newtype a : b = Sub (a => Dict b)
```
but I'm not able to construct a term of type `Collection [Int] x : (Int ~ x)` proving that `Collection [Int] x` entails `Int ~ x`:
```
ghci> Sub Dict :: Collection [Int] x : (Int ~ x)
<interactive>:52:5: error:
• Couldn't match type ‘x1’ with ‘Int’ arising from a use of ‘Dict’
‘x1’ is a rigid type variable bound by
an expression type signature:
forall x1. Collection [Int] x1 : Int ~ x1
at <interactive>:52:13
• In the first argument of ‘Sub’, namely ‘Dict’
In the expression: Sub Dict :: Collection [Int] x : (Int ~ x)
In an equation for ‘it’:
it = Sub Dict :: Collection [Int] x : (Int ~ x)
```
Is this due to overlapping instances or something?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  None 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Can't capture improvement of functional dependencies","status":"New","operating_system":"","component":"None","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["FunctionalDependencies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"[http://www.diku.dk/~paba/pubs/files/serrano15haskellpaper.pdf Type Families with Class, Type Classes with Family] discusses [https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025d9da2a70#pdfinstanceimprovement instance improvement] with the example\r\n\r\n{{{#!hs\r\nclass Collection c e  c > e where\r\n empty :: c\r\n add :: e > c > c\r\n\r\ninstance Collection [a] a where\r\n empty :: [a]\r\n empty = []\r\n\r\n add :: a > [a] > [a]\r\n add = (:)\r\n}}}\r\n\r\nI wondered how to express that `x ~ Int` can be deduced from `Collection [Int] x` using improvement, I first attempted using the [https://hackage.haskell.org/package/constraints constraints] machinery:\r\n\r\n{{{#!hs\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\nnewtype a : b = Sub (a => Dict b)\r\n}}}\r\n\r\nbut I'm not able to construct a term of type `Collection [Int] x : (Int ~ x)` proving that `Collection [Int] x` entails `Int ~ x`:\r\n\r\n{{{\r\nghci> Sub Dict :: Collection [Int] x : (Int ~ x)\r\n\r\n<interactive>:52:5: error:\r\n • Couldn't match type ‘x1’ with ‘Int’ arising from a use of ‘Dict’\r\n ‘x1’ is a rigid type variable bound by\r\n an expression type signature:\r\n forall x1. Collection [Int] x1 : Int ~ x1\r\n at <interactive>:52:13\r\n • In the first argument of ‘Sub’, namely ‘Dict’\r\n In the expression: Sub Dict :: Collection [Int] x : (Int ~ x)\r\n In an equation for ‘it’:\r\n it = Sub Dict :: Collection [Int] x : (Int ~ x)\r\n}}}\r\n\r\nIs this due to overlapping instances or something?","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/11641Allow wildcards for parameters functionally determined (also type synonyms)20190707T18:29:20ZIcelandjackAllow wildcards for parameters functionally determined (also type synonyms)```hs
class F a b  a > b where
foo :: a
 ...
myFoo :: F a b => a
myFoo = foo
```
Since *b* is not used and fully determined by *a* could the restriction on wildcards in constraints be lifted?
```hs
myFoo :: F a _ => a
myFoo = foo
```
and eventually hiding it behind a type synonym:
```hs
type F' a = F a _
myFoo' :: F' a => a
myFoo' = foo
```
I raised this issue at ICFP 2014, I haven't looked into whether dominique's response to [my comment](https://haskellphabricator.global.ssl.fastly.net/D168#4818) applies.

I could achieve similar things with a type family but not quite.

Or CPP :)```hs
class F a b  a > b where
foo :: a
 ...
myFoo :: F a b => a
myFoo = foo
```
Since *b* is not used and fully determined by *a* could the restriction on wildcards in constraints be lifted?
```hs
myFoo :: F a _ => a
myFoo = foo
```
and eventually hiding it behind a type synonym:
```hs
type F' a = F a _
myFoo' :: F' a => a
myFoo' = foo
```
I raised this issue at ICFP 2014, I haven't looked into whether dominique's response to [my comment](https://haskellphabricator.global.ssl.fastly.net/D168#4818) applies.

I could achieve similar things with a type family but not quite.

Or CPP :)https://gitlab.haskell.org/ghc/ghc//issues/11534Allow class associated types to reference functional dependencies20190707T18:29:56ZEdward KmettAllow class associated types to reference functional dependenciesConsider:
```hs
class Foo i j  i > j where
type Bar i :: *
type Bar i = j
```
This is rejected as `j` is not an argument to `Bar`, but when we realize any instance `j` will be a known type, determined by `i`, as told to us by the \ i \> j functional dependency on the class.
This would likely require some sort of extra pass over the instances with class associated types of this form to elaborate them, or a slight modification of the default signature implementation for class associated types.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.3 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Allow class associated types to reference functional dependencies","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["FunctionalDependencies","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider:\r\n\r\n{{{#!hs\r\nclass Foo i j  i > j where\r\n type Bar i :: *\r\n type Bar i = j\r\n}}}\r\n\r\nThis is rejected as `j` is not an argument to `Bar`, but when we realize any instance `j` will be a known type, determined by `i`, as told to us by the  i > j functional dependency on the class.\r\n\r\nThis would likely require some sort of extra pass over the instances with class associated types of this form to elaborate them, or a slight modification of the default signature implementation for class associated types.","type_of_failure":"OtherFailure","blocking":[]} >Consider:
```hs
class Foo i j  i > j where
type Bar i :: *
type Bar i = j
```
This is rejected as `j` is not an argument to `Bar`, but when we realize any instance `j` will be a known type, determined by `i`, as told to us by the \ i \> j functional dependency on the class.
This would likely require some sort of extra pass over the instances with class associated types of this form to elaborate them, or a slight modification of the default signature implementation for class associated types.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.3 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Allow class associated types to reference functional dependencies","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["FunctionalDependencies","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider:\r\n\r\n{{{#!hs\r\nclass Foo i j  i > j where\r\n type Bar i :: *\r\n type Bar i = j\r\n}}}\r\n\r\nThis is rejected as `j` is not an argument to `Bar`, but when we realize any instance `j` will be a known type, determined by `i`, as told to us by the  i > j functional dependency on the class.\r\n\r\nThis would likely require some sort of extra pass over the instances with class associated types of this form to elaborate them, or a slight modification of the default signature implementation for class associated types.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/10675GHC does not check the functional dependency consistency condition correctly20200630T11:14:59ZSimon Peyton JonesGHC does not check the functional dependency consistency condition correctlyConsider
```
{# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
FlexibleInstances, UndecidableInstances,
ScopedTypeVariables #}
class C x a b  a > b where
op :: x > a > b
instance C Bool [x] [x]
instance C Char x y => C Char [x] [Maybe y]
f x = op True [x]
```
Should these two instance declarations be accepted?
The two instances don't *contradict* each other, but neither do they agree as all published work on FDs says they should!
They are *inconsistent* in the sense of Definition 6 of the [FDs through CHRs paper](http://research.microsoft.com/enus/um/people/simonpj/papers/fdchr/jfp06.pdf).
Sadly GHC does not currently reject these as inconsistent. As a result it'll use *both* instance for improvement. In the definition of `f` for example we get
```
C Bool [alpha] beta
```
where `x:alpha` and the result type of `f` is `beta`. By using both instances for improvement we get
```
C Bool [Maybe gamma] [Maybe gamma]
```
That can be solved, so we get
```
f :: Maybe x > [Maybe x]
```
But where did that `Maybe` come from? It's really nothing to do with it.
Examples in the testsuite that exploit this loophole are
```
ghci/scripts ghci047
polykinds T9106
typecheck/should_compile FD4
typecheck/should_compile T7875
```
I'm not sure what the right thing here is.Consider
```
{# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
FlexibleInstances, UndecidableInstances,
ScopedTypeVariables #}
class C x a b  a > b where
op :: x > a > b
instance C Bool [x] [x]
instance C Char x y => C Char [x] [Maybe y]
f x = op True [x]
```
Should these two instance declarations be accepted?
The two instances don't *contradict* each other, but neither do they agree as all published work on FDs says they should!
They are *inconsistent* in the sense of Definition 6 of the [FDs through CHRs paper](http://research.microsoft.com/enus/um/people/simonpj/papers/fdchr/jfp06.pdf).
Sadly GHC does not currently reject these as inconsistent. As a result it'll use *both* instance for improvement. In the definition of `f` for example we get
```
C Bool [alpha] beta
```
where `x:alpha` and the result type of `f` is `beta`. By using both instances for improvement we get
```
C Bool [Maybe gamma] [Maybe gamma]
```
That can be solved, so we get
```
f :: Maybe x > [Maybe x]
```
But where did that `Maybe` come from? It's really nothing to do with it.
Examples in the testsuite that exploit this loophole are
```
ghci/scripts ghci047
polykinds T9106
typecheck/should_compile FD4
typecheck/should_compile T7875
```
I'm not sure what the right thing here is.https://gitlab.haskell.org/ghc/ghc//issues/9210"overlapping instances" through FunctionalDependencies20200630T11:31:37Zrwbarton"overlapping instances" through FunctionalDependenciesThis program prints `("1",2)`, but if you reverse the order of the two instances, it prints `(1,"2")`.
```
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE FunctionalDependencies #}
 extracted from http://lpaste.net/105656
import Control.Applicative
import Data.Functor.Identity
modify :: ((a > Identity b) > s > Identity t) > (a > b) > (s > t)
modify l f s = runIdentity (l (Identity . f) s)
class Foo s t a b  a b s > t where
foo :: Applicative f => (a > f b) > s > f t
instance Foo (x, a) (y, a) x y where
foo f (a,b) = (\fa > (fa,b)) <$> f a
instance Foo (a, x) (a, y) x y where
foo f (a,b) = (\fb > (a,fb)) <$> f b
main = print $ modify foo (show :: Int > String) (1 :: Int, 2 :: Int)
```
Note that the two instances involved `Foo (Int, Int) (String, Int) Int String` and `Foo (Int, Int) (Int, String) Int String` are not actually overlapping. But, they have the same `a`, `b`, and `s` fields and it seems that this makes GHC think that either one is equally valid, thanks to the fundep.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.8.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"\"overlapping instances\" through FunctionalDependencies","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program prints `(\"1\",2)`, but if you reverse the order of the two instances, it prints `(1,\"2\")`.\r\n\r\n{{{\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE FunctionalDependencies #}\r\n\r\n extracted from http://lpaste.net/105656\r\n\r\nimport Control.Applicative\r\nimport Data.Functor.Identity\r\n\r\nmodify :: ((a > Identity b) > s > Identity t) > (a > b) > (s > t)\r\nmodify l f s = runIdentity (l (Identity . f) s)\r\n\r\nclass Foo s t a b  a b s > t where\r\n foo :: Applicative f => (a > f b) > s > f t\r\n\r\ninstance Foo (x, a) (y, a) x y where\r\n foo f (a,b) = (\\fa > (fa,b)) <$> f a\r\n\r\ninstance Foo (a, x) (a, y) x y where\r\n foo f (a,b) = (\\fb > (a,fb)) <$> f b\r\n\r\nmain = print $ modify foo (show :: Int > String) (1 :: Int, 2 :: Int)\r\n}}}\r\n\r\nNote that the two instances involved `Foo (Int, Int) (String, Int) Int String` and `Foo (Int, Int) (Int, String) Int String` are not actually overlapping. But, they have the same `a`, `b`, and `s` fields and it seems that this makes GHC think that either one is equally valid, thanks to the fundep.","type_of_failure":"OtherFailure","blocking":[]} >This program prints `("1",2)`, but if you reverse the order of the two instances, it prints `(1,"2")`.
```
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE FunctionalDependencies #}
 extracted from http://lpaste.net/105656
import Control.Applicative
import Data.Functor.Identity
modify :: ((a > Identity b) > s > Identity t) > (a > b) > (s > t)
modify l f s = runIdentity (l (Identity . f) s)
class Foo s t a b  a b s > t where
foo :: Applicative f => (a > f b) > s > f t
instance Foo (x, a) (y, a) x y where
foo f (a,b) = (\fa > (fa,b)) <$> f a
instance Foo (a, x) (a, y) x y where
foo f (a,b) = (\fb > (a,fb)) <$> f b
main = print $ modify foo (show :: Int > String) (1 :: Int, 2 :: Int)
```
Note that the two instances involved `Foo (Int, Int) (String, Int) Int String` and `Foo (Int, Int) (Int, String) Int String` are not actually overlapping. But, they have the same `a`, `b`, and `s` fields and it seems that this makes GHC think that either one is equally valid, thanks to the fundep.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.8.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"\"overlapping instances\" through FunctionalDependencies","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program prints `(\"1\",2)`, but if you reverse the order of the two instances, it prints `(1,\"2\")`.\r\n\r\n{{{\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE FunctionalDependencies #}\r\n\r\n extracted from http://lpaste.net/105656\r\n\r\nimport Control.Applicative\r\nimport Data.Functor.Identity\r\n\r\nmodify :: ((a > Identity b) > s > Identity t) > (a > b) > (s > t)\r\nmodify l f s = runIdentity (l (Identity . f) s)\r\n\r\nclass Foo s t a b  a b s > t where\r\n foo :: Applicative f => (a > f b) > s > f t\r\n\r\ninstance Foo (x, a) (y, a) x y where\r\n foo f (a,b) = (\\fa > (fa,b)) <$> f a\r\n\r\ninstance Foo (a, x) (a, y) x y where\r\n foo f (a,b) = (\\fb > (a,fb)) <$> f b\r\n\r\nmain = print $ modify foo (show :: Int > String) (1 :: Int, 2 :: Int)\r\n}}}\r\n\r\nNote that the two instances involved `Foo (Int, Int) (String, Int) Int String` and `Foo (Int, Int) (Int, String) Int String` are not actually overlapping. But, they have the same `a`, `b`, and `s` fields and it seems that this makes GHC think that either one is equally valid, thanks to the fundep.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/816Weird fundep behavior (with fallowundecidableinstances)20190707T19:16:47ZnibroWeird fundep behavior (with fallowundecidableinstances)I encounter a strange behavior with functional dependencies. Consider this program
```
class Foo x y  x > y where
foo :: x > y
class Bar x y where
bar :: x > y > Int
instance (Foo x y, Bar y z) => Bar x z where
bar x z = bar (foo x) z
```
Compiling (with 6.4.2, fallowundecidableinstances and fglasgowexts) I get the following error message:
```
Foo.hs:12:0:
Context reduction stack overflow; size = 21
Use fcontextstack20 to increase stack size to (e.g.) 20
`$dBar :: Bar y z' arising from use of `bar' at Foo.hs:13:1113
[... same thing 20 times ...]
`$dBar :: Bar y z' arising from use of `bar' at Foo.hs:13:1113
`bar :: {bar at [y z]}' arising from use of `bar' at Foo.hs:13:1113
When trying to generalise the type inferred for `bar'
Signature type: forall x y z. (Foo x y, Bar y z) => x > z > Int
Type to generalise: x > z > Int
In the instance declaration for `Bar x z'
```
The declaration requires undecidable instances, but I doubt that the problem comes from that. What makes it even more weird is that I can get this to compile, and behave as expected, if I do one of a) declare an instance of Bar for any type, or
b) add an explicit type signature (foo x :: y) in the definition of Bar. The first seems weird since how could a different, unrelated instance affect the typeability of the second instance? The second, b), is weird since by the FD x \> y we should already know that foo x :: y.
Same behavior in GHC 6.4.1. Hugs (with 98 +O) accepts the code.I encounter a strange behavior with functional dependencies. Consider this program
```
class Foo x y  x > y where
foo :: x > y
class Bar x y where
bar :: x > y > Int
instance (Foo x y, Bar y z) => Bar x z where
bar x z = bar (foo x) z
```
Compiling (with 6.4.2, fallowundecidableinstances and fglasgowexts) I get the following error message:
```
Foo.hs:12:0:
Context reduction stack overflow; size = 21
Use fcontextstack20 to increase stack size to (e.g.) 20
`$dBar :: Bar y z' arising from use of `bar' at Foo.hs:13:1113
[... same thing 20 times ...]
`$dBar :: Bar y z' arising from use of `bar' at Foo.hs:13:1113
`bar :: {bar at [y z]}' arising from use of `bar' at Foo.hs:13:1113
When trying to generalise the type inferred for `bar'
Signature type: forall x y z. (Foo x y, Bar y z) => x > z > Int
Type to generalise: x > z > Int
In the instance declaration for `Bar x z'
```
The declaration requires undecidable instances, but I doubt that the problem comes from that. What makes it even more weird is that I can get this to compile, and behave as expected, if I do one of a) declare an instance of Bar for any type, or
b) add an explicit type signature (foo x :: y) in the definition of Bar. The first seems weird since how could a different, unrelated instance affect the typeability of the second instance? The second, b), is weird since by the FD x \> y we should already know that foo x :: y.
Same behavior in GHC 6.4.1. Hugs (with 98 +O) accepts the code.