GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-08-15T15:57:48Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/23827False orphan instance warning for multi-parameter type class instance2023-08-15T15:57:48ZDaneel S. YaitskovFalse orphan instance warning for multi-parameter type class instance## Summary
GHC generates orphan instance warning for a multi-param class instance, which is
located in the same module with one of type parameters, meanwhile another type parameter is
defined in another module. IMHO orphan instance war...## Summary
GHC generates orphan instance warning for a multi-param class instance, which is
located in the same module with one of type parameters, meanwhile another type parameter is
defined in another module. IMHO orphan instance warning is false positive.
## Steps to reproduce
```haskell
-- A.hs
module A where
data TofA
-- C.hs
{-# LANGUAGE FunctionalDependencies #-}
module C where
class Cof2 a b | a -> b where
-- B.hs
module B where
import A
import C
data TofB
instance Cof2 TofA TofB where
```
```
Orphan instance: instance Cof2 TofA TofB
To avoid this
move the instance declaration to the module of the class or of the type, or
wrap the type with a newtype and declare the instance on the new type.
```
## Expected behavior
Absence of orphan instance warning
## Environment
* GHC version used: 9.2.5
Optional:
* Operating System: nix-shell on top of Debian
* https://github.com/NixOS/nixpkgs/archive/aa478e283bb5c73b2cdd2f891251f0d669517b63.tar.gz
* System Architecture: intel 64bitsheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/22385Coverage condition should take functional dependencies in constraints into ac...2022-10-31T20:59:05ZOwen Shepherdowen@owen.cafeCoverage condition should take functional dependencies in constraints into account<!--
READ THIS FIRST: If the feature you are proposing changes the language that GHC accepts
or adds any warnings to `-Wall`, it should be written as a [GHC Proposal](https://github.com/ghc-proposals/ghc-proposals/).
Other features, appr...<!--
READ THIS FIRST: If the feature you are proposing changes the language that GHC accepts
or adds any warnings to `-Wall`, it should be written as a [GHC Proposal](https://github.com/ghc-proposals/ghc-proposals/).
Other features, appropriate for a GitLab feature request, include GHC API/plugin
innovations, new low-impact compiler flags, or other similar additions to GHC.
-->
## Motivation
The following instance is rejected by GHC (without UndecidableInstances) because the coverage condition fails:
```haskell
{-# LANGUAGE FunctionalDependencies #-}
import Data.Functor.Identity
class Dep a b | a -> b where
dep :: a -> b
instance (Dep a a') => Dep (Identity a) (Identity a') where
dep = fmap dep
```
```
• Illegal instance declaration for ‘Dep (Identity a) (Identity a')’
The coverage condition fails in class ‘Dep’
for functional dependency: ‘a -> b’
Reason: lhs type ‘Identity a’
does not determine rhs type ‘Identity a'’
```
`Identity a` does in fact determine `Identity a'`, because `a` determines `a'`, due to the instance's constraint, so I think the code should be accepted by GHC (without UndecidableInstances).
## Proposal
I think that the functional dependencies in the constraints of instances should be taken into account, and the instance should be considered valid.
The coverage condition could be extended[^1] to:
* Let S be the substitution mapping each type variable in the class declaration to the corresponding type in the instance declaration.
* For each functional dependency tvs<sub>left</sub> -> tvs<sub>right</sub>, of the class, every type variable t<sub>dest</sub> in S(tvs<sub>right</sub>) must either appear in S(tvs<sub>left</sub>), or there must exist a t<sub>source</sub> in S(tvs<sub>left</sub>) such that the functional dependencies of the instance's constraints contains a path from t<sub>source</sub> -> t<sub>1</sub> -> ... -> t<sub>n</sub> -> t<sub>dest</sub>
---
[^1]: Original definition taken from https://downloads.haskell.org/~ghc/7.0.1/docs/html/users_guide/type-class-extensions.htmlhttps://gitlab.haskell.org/ghc/ghc/-/issues/22105Odd interation between ambiguity check, instance constraint, and fundeps2022-08-24T22:09:32ZDavid FeuerOdd interation between ambiguity check, instance constraint, and fundeps## Summary
I suspect this might be related to #21149, but it doesn't look quite the same so I figured I'd report it anyway. A custom type error is reported in a situation where it's not at all obvious why the `TypeError` in question is ...## Summary
I suspect this might be related to #21149, but it doesn't look quite the same so I figured I'd report it anyway. A custom type error is reported in a situation where it's not at all obvious why the `TypeError` in question is even being inspected.
## Steps to reproduce
```haskell
{-# language DataKinds, PolyKinds, FunctionalDependencies, AllowAmbiguousTypes, UndecidableInstances #-}
module AmbTE where
import GHC.TypeLits
import Data.Proxy
class xs ~ (hd ': tl) =>
HeadTail (msg :: ErrorMessage) (xs :: [k]) (hd :: k) (tl :: [k])
| xs -> hd tl, hd tl -> xs
instance xs ~ (hd ': tl) => HeadTail msg xs hd tl
instance {-# INCOHERENT #-}
(TypeError msg, '[] ~ (hd ': tl)) => HeadTail msg '[] hd tl
foo :: forall {k} (xs :: [k]) (hd :: k) (tl :: [k]). HeadTail ('Text "whoopsy") xs hd tl => Proxy '(hd, tl)
foo = Proxy
```
This reports
```haskell
AmbTE.hs:10:8: error:
• whoopsy
• In the ambiguity check for ‘foo’
In the type signature:
foo :: forall {k}
(xs :: [k])
(hd :: k)
(tl :: [k]). HeadTail ('Text "whoopsy") xs hd tl => Proxy '(hd, tl)
|
10 | foo :: forall {k} (xs :: [k]) (hd :: k) (tl :: [k]). HeadTail ('Text "whoopsy") xs hd tl => Proxy '(hd, tl)
```
Since I don't see any `'[]` in that type signature, it seems rather surprising to get the type error!
After writing the above, I realized that the fundeps are actually *redundant*. Removing them, surprisingly, makes it compile!
## Expected behavior
I'd expect the above to compile.
## Environment
* GHC version used: 9.4.1
Optional:
* Operating System:
* System Architecture: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/21209Quantified constraint blocks functional dependency2022-03-25T21:37:14ZRichard Eisenbergrae@richarde.devQuantified constraint blocks functional dependencyConsider
```hs
{-# LANGUAGE FunctionalDependencies, QuantifiedConstraints, AllowAmbiguousTypes #-}
module Bug2 where
class C a b | a -> b where
method :: a -> b -> ()
class Truth
instance Truth
f :: (C a b) => a -> ()
f x = method...Consider
```hs
{-# LANGUAGE FunctionalDependencies, QuantifiedConstraints, AllowAmbiguousTypes #-}
module Bug2 where
class C a b | a -> b where
method :: a -> b -> ()
class Truth
instance Truth
f :: (C a b) => a -> ()
f x = method x undefined
g :: (Truth => C a b) => a -> ()
g x = method x undefined
```
`f` is accepted, while `g` is not (in every version of GHC I tested, including HEAD), due to ambiguity of `b` in the call to `method`. But, really, this should be accepted, because the premise of the quantified constraint in the type of `g` is satisfied. The functional dependency should thus choose the type of `undefined` to be `b`.https://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/19415GHC doesn't terminate when solving a weird class instance2022-11-29T08:09:43ZAndrzej RybczakGHC doesn't terminate when solving a weird class instanceThe following:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeApplications #-}
{-#...The following:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Test where
import GHC.TypeLits
data Pet (a :: k) = Pet
{ name :: String
} deriving Show
class SetField (name :: Symbol) s t b | name t -> s b
, name s -> t b where
setField :: b -> s -> t
instance
( SetField "name" (Pet a) (Pet b) String
) => SetField "name" (Pet (a :: k)) (Pet (b :: k')) String where
setField v d = d { name = v }
loop = setField @"name" 'c' (Pet "hi")
```
makes GHC 9.0.1 and HEAD loop. With 8.10.4 it properly terminates with an error:
```
TX.hs:27:8: error:
• Couldn't match type ‘[Char]’ with ‘Char’
arising from a functional dependency between:
constraint ‘SetField "name" (Pet a) (Pet b) Char’
arising from a use of ‘setField’
instance ‘SetField "name" (Pet a1) (Pet b1) String’
at TX.hs:(23,3)-(24,60)
• In the expression: setField @"name" 'c' (Pet "hi")
In an equation for ‘loop’: loop = setField @"name" 'c' (Pet "hi")
|
27 | loop = setField @"name" 'c' (Pet "hi")
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Either changing the kind of `b` to `k` or the instance to
```haskell
instance
( SetField "name" (Pet a) (Pet b) x
, x ~ String
) => SetField "name" (Pet (a :: k)) (Pet (b :: k')) x where
setField v d = d { name = v }
```
makes it terminate again.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/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/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/18406Functional dependency should constrain local inferred type, but does not2022-02-23T13:21:42ZRichard 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...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 `-ddump-tc -fprint-typechecker-elaboration -fprint-explicit-foralls`, 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/derived-refactor) 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 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/18398Inferred type too general, ignoring functional dependencies2022-02-23T13:21:42ZRichard 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...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 ...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/17024Poor interaction between functional dependencies and partial type signatures2020-03-12T13:58:57ZDavid FeuerPoor interaction between functional dependencies and partial type signatures## Summary
A fundep is surprisingly unable to fill in a partial type signature
## Steps to reproduce
```haskell
{-# language TypeFamilies, FunctionalDependencies, GADTs, DataKinds, TypeOperators, ScopedTypeVariables, FlexibleInstances...## Summary
A fundep is surprisingly unable to fill in a partial type signature
## Steps to reproduce
```haskell
{-# language TypeFamilies, FunctionalDependencies, GADTs, DataKinds, TypeOperators, ScopedTypeVariables, FlexibleInstances , UndecidableInstances, PartialTypeSignatures #-}
infixr 6 :::
data HList xs where
HNil :: HList '[]
(:::) :: a -> HList as -> HList (a ': as)
class AppHList ts o f | ts f -> o, ts o -> f where
appHList :: f -> HList ts -> o
instance AppHList '[] o o where
appHList x HNil = x
instance AppHList ts o f => AppHList (t : ts) o (t -> f) where
appHList f (x ::: xs) = appHList (f x) xs
foo :: (a -> b -> c) -> HList '[a, b] -> _
foo = appHList
```
This fails with
```
AbstractList.hs:35:7: error:
• Couldn't match type ‘c’ with ‘w0’
arising from a functional dependency between:
constraint ‘AppHList '[] w0 c’ arising from a use of ‘appHList’
instance ‘AppHList '[] o o’ at AbstractList.hs:29:10-25
‘c’ is a rigid type variable bound by
the inferred type of foo :: (a -> b -> c) -> HList '[a, b] -> w0
at AbstractList.hs:35:1-14
• In the expression: appHList
In an equation for ‘foo’: foo = appHList
• Relevant bindings include
foo :: (a -> b -> c) -> HList '[a, b] -> w0
(bound at AbstractList.hs:35:1)
```
## Expected behavior
I'd expect GHC to fill in `_` with `c`. Indeed, if I leave out the type signature and write
```haskell
foo (f :: a -> b -> c) (args :: HList '[a, b]) = appHList f args
```
then GHC correctly infers `foo :: (a -> b -> c) -> HList '[a, b] -> c`.
## Environment
* GHC version used: 8.6.3
Optional:
* Operating System:
* System Architecture: