GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2022-09-06T11:40:53Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/18851Non-confluence in the solver2022-09-06T11:40:53ZRichard Eisenbergrae@richarde.devNon-confluence in the solverIn #18759 (starting at https://gitlab.haskell.org/ghc/ghc/-/issues/18759#note_306441 and then refined in https://gitlab.haskell.org/ghc/ghc/-/issues/18759#note_306722, but you don't need to read that ticket to understand this one), we ex...In #18759 (starting at https://gitlab.haskell.org/ghc/ghc/-/issues/18759#note_306441 and then refined in https://gitlab.haskell.org/ghc/ghc/-/issues/18759#note_306722, but you don't need to read that ticket to understand this one), we explored various ways of disabling the coverage condition for functional dependencies. In https://gitlab.haskell.org/ghc/ghc/-/issues/18759#note_307486, @simonpj asks whether these techniques can disrupt confluence.
They can. (EDIT: Furthermore, more hammering in this direction discovered non-confluence even *without* functional dependencies. See https://gitlab.haskell.org/ghc/ghc/-/issues/18851#note_318471.)
Here is the example:
```hs
{-# LANGUAGE FunctionalDependencies, FlexibleInstances, UndecidableInstances,
ScopedTypeVariables, TypeFamilies, TypeApplications,
FlexibleContexts, AllowAmbiguousTypes #-}
module Bug where
class C a b | a -> b
instance C Int b => C Int b
class IsInt int
instance int ~ Int => IsInt int
data A
instance Show A where
show _ = "A"
data B
instance Show B where
show _ = "B"
f :: forall a b c int. (Show a, Show b, Show c, C int a, C int b, C int c, IsInt int) => String
f = show (undefined :: c)
g = f @A @B
```
`g` evaluates to `"B"`. If I switch the order of the `C int a` and `C int b` constraints in the type of `f`, `g` will evaluate to `"A"`. Urgh.
(Sidenote: this file needs `AllowAmbiguousTypes`, but there are no ambiguous types here. That bug is reported as #18850.)
What's going on? When calling `f` from `g`, GHC needs to figure out how to instantiate the type variables `a`, `b`, `c`, and `int`, and GHC must find dictionaries to supply for all the class constraints. First, GHC creates unification variables `a0`, `b0`, `c0`, and `int0`. The type applications tell us `a0 := A` and `b0 := B`. Good. Then we have these constraints:
```
[W] w1 : Show A
[W] w2 : Show B
[W] w3 : Show c0
[W] w4 : C int0 A
[W] w5 : C int0 B
[W] w6 : C int0 c0
[W] w7 : IsInt int0
```
GHC processes these in the order given. `w1` and `w2` are easily despatched. `w3` doesn't make any progress at all. Neither does `w4` or `w5`. So we're then in this state:
```
worklist: [W] w6 : C int0 c0
[W] w7 : IsInt int0
inerts: [W] w3 : Show c0
[W] w4 : C int0 A
[W] w5 : C int0 B
```
We then look at `w6`. It doesn't make progress. But then GHC looks at the inerts, and sees that `w4` and `w5` have the same first argument to `C` (`int0`) as the work item `w6`. Because of the functional dependency on `C`, this means that `c0` must match the second argument to `C` in the inert. The problem is that there are *two* such inerts! GHC chooses the last one, arbitrarily. Thus, we get `c0 := B` and carry on. If the constraints were processed in a different order, we'd end up with `c0 := A`. This is classic non-confluence.
Why have `IsInt` here? It's to slow down GHC. If we just wrote an explicit `Int` in the type signature for `f`, then GHC would eagerly solve `w4' : C Int A` and `w5' : C Int B`. When processing `w6' : C Int c0`, GHC wouldn't have any inerts to look at. Instead, it would look at the instance for `C`, which is unhelpful in this case. Indeed, moving the `IsInt int` constraint earlier (before the `C` constraints) in `f`'s type signature causes GHC to error, as it doesn't know how to instantiate `c0`, having lost the hints from the inerts. (More non-confluence!)
What to do? I think the next step is to compare this to the [constraint-handling rules paper](https://www.researchgate.net/profile/Martin_Sulzmann/publication/213885702_Understanding_Functional_Dependencies_via_Constraint_Handling_Rules/links/09e41511297969891f000000.pdf), which proves confluence, and see whether that paper has a mistake, or where GHC violates an assumption in that paper. (Probably the latter: my instance for `C` is very naughty.)https://gitlab.haskell.org/ghc/ghc/-/issues/21864Error messages for functional dependencies are missing critical details2022-07-20T11:10:47ZJade LovelaceError messages for functional dependencies are missing critical details## Summary
GHC's functional dependency errors are quite bad when a downstream usage of a variable resolves to one type, and the definition expects another: they only list the definition site's type. This leads to spooky action at a dist...## Summary
GHC's functional dependency errors are quite bad when a downstream usage of a variable resolves to one type, and the definition expects another: they only list the definition site's type. This leads to spooky action at a distance.
This is felt especially badly in libraries like Esqueleto which use functional dependencies in such a way that type errors in usages of anything defined inside a `from` will appear as a functional dependency error on that builder, rather than where they came from inside, or at the other usage causing the conflicting inference.
I have provided a reproducer of this issue with a tiny query, but this is *significantly* worse in industry code with hundred-line queries. This error is *significantly* worse when you have a query with 25 different `Text` values in it, and the only way to figure out which one was accidentally not `Maybe` is to replace stuff with undefined or otherwise bisect.
The actual issue with the provided code below is that:
```
pure $ li ?. #name
```
should be
```
pure $ li ^. #name
```
where:
```
λ> import Database.Esqueleto.Experimental
λ> :t (^.)
(^.)
:: (PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
λ> :t (?.)
(?.)
:: (PersistEntity val, PersistField typ) =>
SqlExpr (Maybe (Entity val))
-> EntityField val typ -> SqlExpr (Value (Maybe typ))
```
## Steps to reproduce
Please provide a set of concrete steps to reproduce the issue.
Clone the reproducer from https://gitlab.haskell.org/lf-/fundep-repro
The interesting code is reproduced below for convenience:
```haskell
typeError :: MonadIO m => SqlPersistT m (Maybe (Value Text))
typeError = selectOne $ do
(li :& sg) <- from $ table @LineItem
`leftJoin` table @Something
`on` (\(li :& sg) -> just (li ^. #id) E.==. sg ?. #lineItemId)
pure $ li ^. #name
```
```
dev/ghcrepro - [main●] » cabal build
Build profile: -w ghc-9.5.20220714 -O1
In order, the following will be built (use -v for more details):
- lunchline-0.0.0 (exe:lunchline) (file app/Main.hs changed)
Preprocessing executable 'lunchline' for lunchline-0.0.0..
Building executable 'lunchline' for lunchline-0.0.0..
[1 of 3] Compiling Main ( app/Main.hs, /Users/jade/dev/ghcrepro/dist-newstyle/build/aarch64-osx/ghc-9.5.20220714/lunch
line-0.0.0/x/lunchline/build/lunchline/lunchline-tmp/Main.o, /Users/jade/dev/ghcrepro/dist-newstyle/build/aarch64-osx/ghc-9.5.2022
0714/lunchline-0.0.0/x/lunchline/build/lunchline/lunchline-tmp/Main.dyn_o ) [Source file changed]
app/Main.hs:40:13: error:
• Couldn't match type ‘Text’ with ‘Maybe typ0’
arising from a functional dependency between:
constraint ‘Database.Esqueleto.Internal.Internal.SqlSelect
(SqlExpr (Value (Maybe typ0))) (Value Text)’
arising from a use of ‘selectOne’
instance ‘Database.Esqueleto.Internal.Internal.SqlSelect
(SqlExpr (Value a)) (Value a)’
at <no location info>
• In the first argument of ‘($)’, namely ‘selectOne’
In the expression:
selectOne
$ do (li :& sg) <- from
$ table @LineItem
`leftJoin`
table @Something
`on`
(\ (li :& sg) -> just (li ^. #id) E.==. sg ?. #lineItemId)
pure $ li ?. #name
In an equation for ‘typeError’:
typeError
= selectOne
$ do (li :& sg) <- from
$ table @LineItem
`leftJoin`
table @Something
`on`
(\ (li :& sg)
-> just (li ^. #id) E.==. sg ?. #lineItemId)
pure $ li ?. #name
|
40 | typeError = selectOne $ do
| ^^^^^^^^^
app/Main.hs:41:19: error:
• Couldn't match type: Entity LineItem
with: Maybe (Entity val0)
arising from a functional dependency between:
constraint ‘Database.Esqueleto.Experimental.From.ToFrom
(From
(SqlExpr (Entity LineItem) :& SqlExpr (Maybe (Entity Something))))
(SqlExpr (Maybe (Entity val0))
:& SqlExpr (Maybe (Entity Something)))’
arising from a use of ‘from’
instance ‘Database.Esqueleto.Experimental.From.ToFrom (From a) a’
at <no location info>
• In the first argument of ‘($)’, namely ‘from’
In a stmt of a 'do' block:
(li :& sg) <- from
$ table @LineItem
`leftJoin`
table @Something
`on` (\ (li :& sg) -> just (li ^. #id) E.==. sg ?. #lineItemId)
In the second argument of ‘($)’, namely
‘do (li :& sg) <- from
$ table @LineItem
`leftJoin`
table @Something
`on` (\ (li :& sg) -> just (li ^. #id) E.==. sg ?. #lineItemId)
pure $ li ?. #name’
|
41 | (li :& sg) <- from $ table @LineItem
| ^^^^
```
## Expected behavior
What do you expect the reproducer described above to do?
I would like to know where the conflicting usage is. For instance, I would like to see that that the other direction of bad inference came from `li ^. #name`.
## Environment
* GHC version used:
I grabbed HEAD to confirm this still is a bug, but it also happens on 9.0, 9.2.
```
ghc --version
The Glorious Glasgow Haskell Compilation System, version 9.5.20220714
```
Optional:
* Operating System: macOS
* System Architecture: aarch64https://gitlab.haskell.org/ghc/ghc/-/issues/21779"Wiggly arrows" as an alternative to functional dependencies2022-09-27T07:00:35ZAdam Gundry"Wiggly arrows" as an alternative to functional dependencies"Wiggly arrows" are an idea I've been exploring (originally with @simonpj and subsequently with a few others) for an alternative to functional dependencies, used merely to guide type inference. Hopefully this could provide a replacement ..."Wiggly arrows" are an idea I've been exploring (originally with @simonpj and subsequently with a few others) for an alternative to functional dependencies, used merely to guide type inference. Hopefully this could provide a replacement for some of the current "abuses" of fundeps, and allow fundeps to be subsequently made stricter (e.g. by translation to type families). One motivating example is extending `HasField` with a type-changing `SetField`.
I've started writing up the idea on the wiki (https://gitlab.haskell.org/ghc/ghc/-/wikis/Functional-dependencies-in-GHC/Wiggly-arrows) and would welcome feedback. This will need a full GHC proposal, of course.https://gitlab.haskell.org/ghc/ghc/-/issues/21703cc_fundeps does not really work2022-11-29T08:42:49ZSimon Peyton Jonescc_fundeps does not really work@abel reports [here](https://gitlab.haskell.org/ghc/ghc/-/issues/18851#note_433870): Here might be a case in the wild from some 2010/11 Haskell legacy code. Compilation succeeds with GHC <= 9.2.3, but breaks with GHC 9.4:
```
$ cabal in...@abel reports [here](https://gitlab.haskell.org/ghc/ghc/-/issues/18851#note_433870): Here might be a case in the wild from some 2010/11 Haskell legacy code. Compilation succeeds with GHC <= 9.2.3, but breaks with GHC 9.4:
```
$ cabal install helf-0.2021.8.12 -w ghc-9.4.0.20220523 --allow-newer
[33 of 35] Compiling Closures ( src/Closures.hs, dist/build/helf/helf-tmp/Closures.o )
src/Closures.hs:101:13: error:
• No instance for (MonadCheckExpr
fvar0 Val Env EvalM (ReaderT SigCxt Err))
arising from a use of ‘doEval’
• In the first argument of ‘(.)’, namely ‘doEval’
In the expression: doEval . prettyM
In an equation for ‘prettyM’: prettyM = doEval . prettyM
|
101 | prettyM = doEval . prettyM
| ^^^^^^
```
The fix is to insert a type application `doEval @Head` to resolve `fvar0`: https://github.com/andreasabel/helf/commit/ee86c0b47a6db40930ae0f2f4b7ee0a6b5b001c1
## Diagnosis
I investigated. Sadly it is a real bug, concerning fundeps, arising from the fix for #19415. `Note [Fundeps with instances]` in GHC.Tc.Solver.Interact says:
```
Note [Fundeps with instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
...
* There is a flag in CDictCan (cc_fundeps :: Bool)
* cc_fundeps = True means
a) The class has fundeps
b) We have not had a successful hit against instances yet
* In doTopFundepImprovement, if we emit some constraints we flip the flag
to False, so that we won't try again with the same CDictCan. In our
example, dwrk will have its flag set to False.
...
Easy! What could go wrong?
* Maybe the class has multiple fundeps, and we get hit with one but not
the other. Per-fundep flags?
* Maybe we get a hit against one instance with one fundep but, after
the work-item is instantiated a bit more, we get a second hit
against a second instance. (This is a pretty strange and
undesirable thing anyway, and can only happen with overlapping
instances; one example is in Note [Weird fundeps].)
But both of these seem extremely exotic, and ignoring them threatens
completeness (fixable with some type signature), but not termination
(not fixable). So for now we are just doing the simplest thing.
```
Alas, this program tickles the first of these "what could go wrong" bullets. Specifically, we have
```
class ... => MonadEval head val env m | val -> head, m -> val, m -> env where
instance ... => MonadEval Head Val Env m where
```
This is pretty bizarre. The fundeps say that in the constraint `MonadEval h v e m`, then
*for any `m`**, we must have `v~Val`, and `e~Env`; and hence, transitively `h~Head`.
Bonkers. But there it is.
(`UndecidableInstances` etc are all on.)
Now we are trying to solve
```
[W] MonadEval h0 v0 e0 EvalM
```
where `h0`, `v0`, `e0` are all unification variables. So GHC generates `v0~Val` and `e0~Env`.
But it does not generate `h0~Head` because the second parameter is not (yet) `Val`.
Now we unify, but *alas* because of `Note [Fundeps with instances]` we no longer look
at fundeps for this constraint, and thereby never emit `h0~Head`.
## Workaround
Simple fix: make the class decl make explicit the depdency of `head` from `m`:
```
class ... => MonadEval head val env m | val -> head, m -> val, m -> env, m -> head where
```
It's a bit silly, because it's implied, but it solves the problem.
## What to do
I am unsure if it's worth losing sleep over this one, given that
* the example is pretty bizarre
* the fix is very easy
Still, I dislike the solver not taking advantage of a useful fundep. One alternative
would be to elaborate `cc_fundeps` to a `[Bool]`, one for each fundep. Not really hard,
and maybe easier than debugging this next time!
Better ideas welcome.9.4.4Simon Peyton JonesRichard Eisenbergrae@richarde.devSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/20238deriving via can't coerce through functional dependencies2021-08-24T14:39:51ZCarter Schonwaldderiving via can't coerce through functional dependencies@RyanGlScott @Icelandjack
at least in ghc 8.10.4, i've hit the following error
```
error:
• Couldn't match type ‘[BSC.ByteString]’ with ‘HoldingKey’
arising from a functional dependency between:
constraint ‘Mon...@RyanGlScott @Icelandjack
at least in ghc 8.10.4, i've hit the following error
```
error:
• Couldn't match type ‘[BSC.ByteString]’ with ‘HoldingKey’
arising from a functional dependency between:
constraint ‘MonadOverlay
HoldingKey
BSC.ByteString
heapval
(OverlayM
(TP.TrieMap BSC.ByteString heapval)
(VariableScopeM (IndexVarMap heapval) m))’
arising from the 'deriving' clause of a data type declaration
instance ‘MonadOverlay [k] k v (OverlayM (TP.TrieMap k v) m1)’
at <no location info>
• When deriving the instance for (MonadOverlay
HoldingKey
BSC.ByteString
heapval
(ErasedInterpreterM heapval m))
|
422 | deriving (MonadOverlay HoldingKey BSC.ByteString heapval)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
they definitely are coercible
```
newtype HoldingKey = HoldingKey {getPath :: [BSC.ByteString]}
```
the deriving via i'm doing is (based on your unary constraint remark)
```
deriving (MonadOverlay HoldingKey BSC.ByteString heapval)
via OverlayM (TP.TrieMap BSC.ByteString heapval) (VariableScopeM (IndexVarMap heapval) m )
```
where the underlying instance i'm coercing from is defined at the bottom of this snippet
```
class PartialTrieMap (mp :: * -> * -> *) k {- k v -> a-} where
readMap :: mp k v -> [k] -> Maybe v
writeMap :: mp k v -> [k] -> v -> mp k v
{-# MINIMAL readMap,writeMap#-}
instance (LBM.OrdMap DMS.Map k , Ord k) => PartialTrieMap (TP.TrieMap ) k where
readMap = \ mp v -> TP.lookup v mp
writeMap = \ mp k v -> TP.insert k v mp
class (Monad m)=> MonadOverlay k segment v m | m -> k v , k -> segment where
overRead :: k -> m (Maybe v)
overWrite :: k -> v -> m ()
------ this instance below!
instance (Monad m,Ord k,PartialTrieMap TP.TrieMap k ) => MonadOverlay [k] k v (OverlayM (TP.TrieMap k v) m) where
overRead = \ key -> OverlayedM $ \ rd st ->
do
cacheread <- return $ readMap st key ;
case cacheread of
Just _v -> return (cacheread,st)
Nothing -> do coldRead <- return $ readMap rd key ; return (coldRead,st)
overWrite = \ key val -> OverlayedM $ \ _rd st -> return ((), writeMap st key val )
```
i can distill this down into a smaller example if neededhttps://gitlab.haskell.org/ghc/ghc/-/issues/20064When does GHC quantify over variables fully determined by fundeps?2022-09-06T11:36:56Zsheafsam.derbyshire@gmail.comWhen does GHC quantify over variables fully determined by fundeps?Consider the following example:
```haskell
{-# LANGUAGE FlexibleContexts, FunctionalDependencies, NoMonomorphismRestriction #-}
data AB a b = AB
class C a b | a -> b where
meth :: AB a b -> b
ab :: AB Int b
ab = AB
--foo :: C Int ...Consider the following example:
```haskell
{-# LANGUAGE FlexibleContexts, FunctionalDependencies, NoMonomorphismRestriction #-}
data AB a b = AB
class C a b | a -> b where
meth :: AB a b -> b
ab :: AB Int b
ab = AB
--foo :: C Int b => b
foo = meth ab
```
GHC is able to infer the commented type for `foo`. Some other test cases which present the same behaviour are `tc231` where we have
```haskell
data Z a = ...
data Q s a chain = ...
class Zork s a b | a -> b where ...
```
where GHC will infer the following type for `foo`:
```
foo :: Zork s (Z [Char]) b => Q s (Z [Char]) chain -> ST s ()
foo = ...
```
and `tcfail093`, where we have
```haskell
class Call c h | c -> h where ...
```
and GHC will infer the following type for `dup`:
```haskell
dup :: Call (IO Int) h => () -> Int -> h
dup = ...
```
@rae's patch to remove Deriveds changes all these programs to throw type errors. So for the first one we get:
```
* No instance for (C Int b0) arising from a use of `meth'
* In the expression: meth ab
In an equation for `foo': foo = meth ab
|
12 | foo = meth ab
| ^^^^^^^
```
for `tc231` we get:
```
* No instance for (Zork s (Z [Char]) b0)
arising from a use of `huh'
* In the expression: huh (s b)
In an equation for `foo': foo b = huh (s b)
```
and for `tcfail093` we get:
```
* No instance for (Call (IO Int) h0) arising from a use of `call'
* In the expression: call primDup
In an equation for `dup': dup () = call primDup
```
Pinging @simonpj for thoughts, as Simon committed a change that allowed `tc231` and `tcfail093` to both typecheck, justified by the (now removed) [Note [Important subtlety in oclose]](https://gitlab.haskell.org/ghc/ghc/-/commit/ecddaca17dccbe1d0b56220d838fce8bc4b97884#ef94ac21ad807a07e51886b7e2a0abf22cd9772f_82_79). That note remarks that cases such as `tcfail093` are "right on the borderline", so it seems reasonable to revert back to throwing an error.https://gitlab.haskell.org/ghc/ghc/-/issues/19126Dubious FunDep behaviour, even for a 'textbook' example with non dodgy extens...2021-02-16T20:34:27ZAnthony ClaydenDubious FunDep behaviour, even for a 'textbook' example with non dodgy extensions## Summary
GHC's behaviour for a 'textbook' FunDep instance (without the known-to-be-dodgy extensions) is not as per the theory in the 'FunDeps via CHRs' 2006 paper.
In itself this is not problematic; there's an easy workaround; indeed...## Summary
GHC's behaviour for a 'textbook' FunDep instance (without the known-to-be-dodgy extensions) is not as per the theory in the 'FunDeps via CHRs' 2006 paper.
In itself this is not problematic; there's an easy workaround; indeed FunDepers probably take it 'this is how GHC works'. But the workaround needs `UndecidableInstances`, which removes any confidence about confluence and termination across all instances in the module.
(I'm documenting this in context of a whirl of recent issues #18759, #18851 and ref [this comment](https://github.com/ghc-proposals/ghc-proposals/pull/374#issuecomment-750491151) on a github proposal.)
## Steps to reproduce
Consider this classic textbook FunDep, from the Jones 2000 paper
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts #-}
class Collects e ce | ce -> e where
member :: e -> ce -> Bool
-- etc
instance Eq e => Collects e [e] where
member = elem
x1 = member True [False, False, True] -- ===> True
x2 = member undefined ([] :: [Bool]) -- ===> False
The FunDeps via CHRs paper [Section 4.2/Fig 2 translation rules] says that instance should be equivalent to this:
{-# LANGUAGE UndecidableInstances, GADTs #-}
class CollectF2 e ce | ce -> e where
memberF2 :: e -> ce -> Bool
instance (a ~ e, Eq e) => CollectF2 a [e] where
memberF2 = elem
Using `~` constraint to explicitly apply the type improvement (needs `GADTs`), and bare tyvar `a` in the instance head as target for the improvement (needs `UndecidableInstances`).
## Expected behavior
This instance and its non-confluent consequence should be rejected:
instance {-# OVERLAPPABLE #-} (a ~ ()) => Collects a [e] where
member _ _ = False
x3 = member () [False, False, True] -- ===> False
Compare:
instance {-# OVERLAPPABLE #-} (a ~ ()) => CollectF2 a [e] where
memberF2 _ _ = False
-- error: Duplicate instance declarations:
Best practice for using FunDeps (see examples cited in the github comments) is to use instance heads in a style per `CollectF2` with a bare fresh tyvar as the target. This needs `UndecidableInstances` even though the type improvement via `~` is perfectly decidable. That extension is module-wide, and allows exactly the non-confluence with that `instance (a ~ ()) => Collects a [e]` it was seeking to avoid. FunDepers must be disciplined in how they write instances.
## Environment
* GHC version used: 8.10.2
Optional:
* Operating System: Windows 8
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/19043Functional dependencies (for classes or type familes alike) can not refine gi...2021-01-19T09:02:54ZJohn EricsonFunctional dependencies (for classes or type familes alike) can not refine given equality constraints## Motivation
Consider these two versions of `foo`:
```haskell
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeOperators #-}
import Data.Type.Equalit...## Motivation
Consider these two versions of `foo`:
```haskell
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeOperators #-}
import Data.Type.Equality
type family Foo a = r | r -> a
fooTF :: (Foo a ~ Foo a') => a :~: a'
fooTF = Refl
class FooC a r | r -> a
fooC :: (FooC a r, FooC a' r) => a :~: a'
fooC = Refl
```
However, both fail to type check (as of 8.1):
```
loop.hs:11:9: error:
• Could not deduce: a ~ a'
from the context: Foo a ~ Foo a'
bound by the type signature for:
fooTF :: forall a a'. (Foo a ~ Foo a') => a :~: a'
at loop.hs:10:1-37
‘a’ is a rigid type variable bound by
the type signature for:
fooTF :: forall a a'. (Foo a ~ Foo a') => a :~: a'
at loop.hs:10:1-37
‘a'’ is a rigid type variable bound by
the type signature for:
fooTF :: forall a a'. (Foo a ~ Foo a') => a :~: a'
at loop.hs:10:1-37
Expected type: a :~: a'
Actual type: a :~: a
• In the expression: Refl
In an equation for ‘fooTF’: fooTF = Refl
• Relevant bindings include
fooTF :: a :~: a' (bound at loop.hs:11:1)
|
11 | fooTF = Refl
| ^^^^
loop.hs:16:8: error:
• Couldn't match type ‘a’ with ‘a'’
‘a’ is a rigid type variable bound by
the type signature for:
fooC :: forall a r a'. (FooC a r, FooC a' r) => a :~: a'
at loop.hs:15:1-41
‘a'’ is a rigid type variable bound by
the type signature for:
fooC :: forall a r a'. (FooC a r, FooC a' r) => a :~: a'
at loop.hs:15:1-41
Expected type: a :~: a'
Actual type: a :~: a
• In the expression: Refl
In an equation for ‘fooC’: fooC = Refl
• Relevant bindings include
fooC :: a :~: a' (bound at loop.hs:16:1)
|
16 | fooC = Refl
| ^^^^
```
I would have thought that trying to decompose qualities like this is the very essence of what functional dependencies are for, so I am quite confused.
## Proposal
Make this work. I'm not sure exactly what this entails, because I don't currently understand the difference between what functional dependencies *do* do and this.
I will note, however, that doing so perhaps makes existing issues with functional dependencies like #10675 worse because we could get unsound equality evidence to do unsafe coercions with.https://gitlab.haskell.org/ghc/ghc/-/issues/18759Types with different forall placements don't unify with QL ImpredicativeTypes2022-06-30T00:52:03ZAndrzej RybczakTypes with different forall placements don't unify with QL ImpredicativeTypesThe following program:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE KindSignatures...The following program:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}
import GHC.TypeLits
main :: IO ()
main = pure ()
data X = X { x :: forall a. a -> a }
class HasField (name :: Symbol) s a | name s -> a where
getField :: s -> a
instance a ~ (forall x. x -> x) => HasField "x" X a where
getField = x
getX_Ok_sel :: X -> forall a. a -> a
getX_Ok_sel = x
getX_Bad_sel :: forall a. X -> a -> a
getX_Bad_sel = x
getX_Ok_class :: X -> forall a. a -> a
getX_Ok_class = getField @"x"
getX_Bad_class :: forall a. X -> a -> a
getX_Bad_class = getField @"x"
getX_Bad_classUsage :: String
getX_Bad_classUsage = getField @"x" (X id) "hello world"
```
produces errors with GHC 9.1.0.20200927:
```
unknown@electronics _build $ ./ghc-stage1 it.hs
[1 of 1] Compiling Main ( it.hs, it.o )
it.hs:29:16: error:
• Couldn't match type: forall a1. a1 -> a1
with: a -> a
Expected: X -> a -> a
Actual: X -> forall a. a -> a
• In the expression: x
In an equation for ‘getX_Bad_sel’: getX_Bad_sel = x
• Relevant bindings include
getX_Bad_sel :: X -> a -> a (bound at it.hs:29:1)
|
29 | getX_Bad_sel = x
| ^
it.hs:35:18: error:
• Couldn't match type: a -> a
with: forall x. x -> x
arising from a use of ‘getField’
• In the expression: getField @"x"
In an equation for ‘getX_Bad_class’: getX_Bad_class = getField @"x"
• Relevant bindings include
getX_Bad_class :: X -> a -> a (bound at it.hs:35:1)
|
35 | getX_Bad_class = getField @"x"
| ^^^^^^^^
it.hs:38:23: error:
• Couldn't match type: String -> String
with: forall x. x -> x
arising from a use of ‘getField’
• In the expression: getField @"x" (X id) "hello world"
In an equation for ‘getX_Bad_classUsage’:
getX_Bad_classUsage = getField @"x" (X id) "hello world"
|
38 | getX_Bad_classUsage = getField @"x" (X id) "hello world"
```
The `Bad_sel` and `Bad_class` issues look very similar, but produce error messages with flipped actual and expected types, which confuses me a bit.
`Bad_classUsage` looks like a consequence of `Bad_class` not working.https://gitlab.haskell.org/ghc/ghc/-/issues/18400Instances do not respect functional dependency, yet are accepted2020-11-13T13:39:12ZRichard 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...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/17765Documentation for FunctionalDependencies is misleading/incomplete (and their ...2020-02-20T16: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 a...## 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:10-14
• 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: [-Wsimplifiable-class-constraints]
• 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: [-Wsimplifiable-class-constraints]
• 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?2020-05-19T12: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 th...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 poly-kinded, but it would be inferred to be poly-kinded, 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 derived instances that violate functional dependencies2021-10-30T13:54:47ZAlexis KingGHC accepts derived 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...## 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’
Un-determined 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) accepted2019-07-07T18: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 & R...# 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/hugs98-plus-Sep2006/blob/master/src/static.c) is, for each FunDep in the class decl:
* the tyvars to the right of each `->` must be non-empty;
* 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 long-standing 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 tin2019-03-23T11: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 {...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 real-life example where I bumped into this rejection.)https://gitlab.haskell.org/ghc/ghc/-/issues/15927Weird interaction between fundeps and overlappable instances2022-09-06T11:41:06ZDarwin226Weird 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 (...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 Dependencies2020-10-30T21:05:15ZAntCUndependable DependenciesConsider
```hs
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
GADTs, FlexibleInstances, FlexibleContexts,
UndecidableInstances #-}
data Hither = Hither deriving (Eq, Show, Read) -- just th...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.1-beta1 |
| 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.1-beta1","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/15351QuantifiedConstraints ignore FunctionalDependencies2020-12-03T08:24:56ZaaronvargoQuantifiedConstraints ignore FunctionalDependenciesThe following code fails to compile:
```hs
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FunctionalDependencies #-}
class C a b | a -> b where
foo :: a -> b
bar :: (forall a. C (f a) Int) => f a -> String
bar = show . foo
```
...The following code fails to compile:
```hs
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FunctionalDependencies #-}
class C a b | a -> b where
foo :: a -> b
bar :: (forall a. C (f a) Int) => f a -> String
bar = show . foo
```
```
• Could not deduce (Show a0) arising from a use of ‘show’
...
The type variable ‘a0’ is ambiguous
• Could not deduce (C (f a) a0) arising from a use of ‘foo’
...
The type variable ‘a0’ is ambiguous
```
Yet it ought to work, since this is perfectly fine with top-level instances:
```hs
instance C [a] Int where ...
baz :: [a] -> String
baz = show . foo
```https://gitlab.haskell.org/ghc/ghc/-/issues/14778FunDep origin not correctly attributed2019-07-07T18: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...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 givens2019-07-07T18: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...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 top-level 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 top-level 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":[]} -->