@ezyang Ah, there seems to be an important detail that I left out: I also used the same source directory for each library as well:
library foo
hssourcedirs: src
defaultlanguage: Haskell2010
builddepends: base
signatures: A
exposedmodules: Foo, IllKindedA
library bar
hssourcedirs: src
builddepends: base , foo
exposedmodules: Bar
mixins: foo (Foo as Bug) requires (A as IllKindedA)
Everything works correctly (I think) if I use different directories.
The panic came about due to me attempting to try backpack while having no idea what I was doing.
Oops, it seems this only happened because I foolishly had IllKindedA
in the same library as A
:
library foo
builddepends: base
signatures: A
exposedmodules: Foo, IllKindedA
library bar
builddepends: base, foo
exposedmodules: Bar
mixins: foo (Foo as Bug) requires (A as IllKindedA)
It's still a bug though.
Given the following:
{# language KindSignatures #}
signature A where
data A :: *
module Foo where
import A
foo :: A > A
foo = id
module IllKindedA where
type A = Maybe
GHC allows the signature A
to be instantiated with IllKindedA
:
mixins: foo (Foo as Bug) requires (A as IllKindedA)
Using the resulting module can cause odd errors or a panic. E.g. the following causes a panic:
module Bar where
import Bug
bar = foo
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.2 for x86_64unknownlinux):
getRuntimeRep
A :: * > *
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:2049:18 in ghc:Type
Replying to [ticket:15347#comment:157453 simonpj]:
Not allowing functions in the instance head not to do with ambiguity; it's to do with coherence
But is this an issue for QCs, which can't introduce incoherence? Does it matter if two QCs might overlap, as long as locally we can't tell that they do? Suppose we had:
type family F a = r  r > a
type family G a = r  r > a
foo :: forall b. (forall a. Eq (F a), forall a. Eq (G a)) => Dict (Eq (F b))
foo = Dict
While F b
and G b
might overlap for some particular b
, locally only one instance can be used to solve Eq (F b)
, since we don't know whether G b ~ F b
. Since the two instances are guaranteed to be coherent, wouldn't it be fine to simply pick the one that matches? (If both were to match then the program would still be rejected).
Likewise for the case with noninjective independent type families:
foo :: forall b. (forall t. C (F b) [t], forall t. C (G b) [t]) => Dict (C (F b) [Int])
The first instance should just be used, since it's the only one that matches given the knowledge available locally.
How does the compiler currently deal with type families in nonquantified constraints? What makes it more difficult to allow them in QCs?
Can you distil a small example that shows the utility of having a function in the head?
For now I have no use case for the injective type family case, and only really care about the independent family case. I'll try and come up with a simpler example than the category one.
So, maybe a quantified constraint with a function in the head is just "parked", but it wakes up if the function can be reduced.
This is much less useful than what I want, though I suppose it might help in some small minority of cases.
Replying to [ticket:15347#comment:157435 simonpj]:
I thought I'd once seen a ticket for this, and I've managed to find it: see #3490, where you write:
The easiest way forward is to reexpress your program using type functions
Also, on second thought, what I said in ticket:15347#comment:157437 won't work.
Replying to [ticket:15347#comment:157435 simonpj]:
Really? What wrong with this?
Not in scope: type variable ‘ft’
The superclass isn't allowed to mention variables which don't appear in the head, even if they're already determined by other parameters. The solution to this limitation has been "use type families", which leads us to this issue.
I don't see why that is though. Why can't ft
be made an implicit parameter to the class?
If it were possible to explicitly bind the implicit parameters of a class, perhaps we could write something like:
class forall ft. (ft ~ F t, forall a. Eq a => Eq (ft a)) => C t
Hmm, it is possible to make ft
implicit using a proxy though:
class (ft ~ F t, forall a. Eq a => Eq (ft a)) => C (p :: Proxy ft) t where
type F t :: * > *
 this works
foo :: forall t a. (C 'Proxy t, Eq a) => Dict (Eq (F t a))
foo = Dict
This still requires adding a parameter, but would only require adding one to each class rather than potentially several, as we can use a single proxy for all of the extra parameters.
Replying to [ticket:15347#comment:157432 simonpj]:
Yes, sorry!
That is, so far I do not understand why floating out type families (a straightforward sourcetosource transformation that does not change the number of class parameters) would sacrifice a major benefit.
It requires changing the number of class parameters when the quantified constraint appears as a superclass. Suppose we would like to write:
class (forall a. Eq a => Eq (F t a)) => C t where
type F t :: * > *
where the type family F t
in the quantified constraint is independent of the quantified a
. In order to float this type family out, we need to add a new parameter to the class, ft
, and make it equal to F t
:
class (ft ~ F t, forall a. Eq a => Eq (ft a)) => C ft t where
type F t :: * > *
Furthermore, this parameter can never be instantiated with a type family without once again breaking the quantified constraint. E.g. if we write
class C (F t) t => D t
then the inherited quantified constraint will contain a type family, and will no longer work.
Replying to [ticket:15347#comment:156428 simonpj]:
A few things:
First, there's probably another way to do this without a freevariable analysis: float type families out when they appear in wanted constraints. E.g. in foo
, the floating would happen because F b
appears in the wanted constraint, not because it's independent of the forall'd variables in the given quantified constraint. Would something like that be more feasible?
Second,
Consider this:
type family F a type instance F Int = Bool instance Eq a => Eq (F a) where ...
Should we allow this? Obviously not. It's like allowing...
Indeed, but this is an argument for disallowing ambiguity, not for disallowing type families. In your Eq
example, a
is ambiguous since F
may not be injective. (likewise, xs
and ys
are ambiguous in the map
example since (++)
isn't injective). Not all uses of type families cause such ambiguity, and the compiler already has a perfectly good ambiguity check which can determine whether they do. Some cases where they don't are:
forall a. C (F a) [a]
For toplevel instances there may be coherence issues with allowing type families even when they don't cause ambiguity, but such issues don't apply to QCs, which can't introduce incoherence.
So why not allow type families in QCs, but require that the quantified variables be unambiguous?
Third, working around this by manually floating out type families can be hugely painful, as it requires sacrificing one of the major benefits of type families, namely the ability to avoid passing around extra class parameters which are already determined by other parameters. The basic problem is this: suppose we have a class:
class (forall a. Eq a => Eq (f a)) => C f t  t > f
Currently, the parameter f
can never be instantiated with a type family without breaking the quantified constraint. This means the extra parameter needs to be repeated throughout the code for the QC to continue to work, despite the fact that f
is already determined by t
.
Consider the following encoding of categories and functors, which makes use of type families:
type Hom k = k > k > Type
 Natural transformations
data (==>) (p :: Hom i) (q :: Hom j) (f :: i > j) (g :: i > j)
class ( Category (Op p)
, Op (Op p) ~ p
, Ob (Op p) ~ Ob p
, FunctorOf' (Op p) (p ==> (>)) p
, forall a. Ob p a => FunctorOf' p (>) (p a)
) => Category (p :: Hom k) where
type Ob p :: k > Constraint
type Op p :: Hom k
 FunctorOf without superclasses, to work around issues with UndecidableSuperClasses
class FunctorOf' (p :: Hom i) (q :: Hom j) (f :: i > j)  f > p q
 FunctorOf' with proper superclasses
class ( FunctorOf' p q f
, Category p
, Category q
, forall a. Ob p a => Ob q (f a)
) => FunctorOf p q f
instance ( FunctorOf' p q f
, Category p
, Category q
, forall a. Ob p a => Ob q (f a)
) => FunctorOf p q f
Note that Category p
has a superclass Category (Op p)
, which has a superclass:
 noting that Ob (Op p) ~ Ob p
forall a. Ob p a => FunctorOf' (Op p) (>) (Op p a)
and that the superclasses of FunctorOf p q f
include:
forall a. Ob p a => Ob q (f a)
forall a. Ob p a => FunctorOf' (Op p) (>) (Op p a)
forall a. Ob q a => FunctorOf' (Op q) (>) (Op q a)
All of these have independent type families in the heads. Floating them out manually requires doubling the number of class parameters for both Category
and FunctorOf
:
class (..., op ~ Op p) => Category op (p :: Hom k) where ...
class ( FunctorOf' p q f
, Category opP p
, Category opQ q
, obQ ~ Ob q
, forall a. Ob p a => obQ (f a)
) => FunctorOf opP p opQ q obQ f
These parameters will spread throughout all of the code. Subclasses will add yet more parameters, and will never be able to use type families for anything which is a functor or a category, without sacrificing some QCs. Types will be lost in a sea of parameters.
This ends up being more painful than just using Dict
s.
Replying to [ticket:15351#comment:156490 simonpj]:
Would anyone like to fix this?
How difficult would it be? I might like to try, but I've never contributed to GHC before. I could see it being pretty simple since most of the logic should already exist for toplevel instances, but I wouldn't know. And I might need some handholding...
It's intriguing  I never expected people to explore the outer limits of quantified constraints so rapidly.
I would guess this is partly because we could already (somewhat painfully) manually represent such constraints with Dict
s, so we already had some idea of what they might be useful for, and want them to be able to do everything we can do with Dict
s (though that turns out to be unreasonable).
I came across this particular issue while trying to work around #15347, but I'll write more about that on that ticket (at some point. Maybe after I can get my stupid example to work).
Ah, indeed it is!
This could be related to #15343.
The following code fails to compile with GHC 8.6.0.20180627, but does compile with 8.4:
{# LANGUAGE TypeInType #}  or PolyKinds
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE TypeFamilies #}
import Data.Kind
class C (x :: Type) (y :: k) where
type F y
• Expected a type, but ‘k’ has kind ‘k’
• In the kind ‘k’

7  class C (x :: Type) (y :: k) where
 ^
Yet all of the following slightly different examples still do compile:
 remove `x`
class C0 (y :: k) where type F0 y
 remove `F`
class C1 (x :: Type) (y :: k)
 remove the kind annotation from `x`
class C2 x (y :: k) where type F2 y
 switch the order of `x` and `y`
class C3 (y :: k) (x :: Type) where type F3 y
 make `k` an explicit parameter, with or without a kind annotation
class C4 k (x :: Type) (y :: k) where type F4 y
class C5 (k :: Type) (x :: Type) (y :: k) where type F5 y
 add a new parameter *with no kind annotation*
class C6 z (x :: Type) (y :: k) where type F6 y
Here's also my original example which failed to compile:
type Hom k = k > k > Type
type family Ob (p :: Hom k) :: k > Constraint
class ( obP ~ Ob p
, opP ~ Dom p
, obQ ~ Ob q
, opQ ~ Dom q
, p ~ Dom f
, q ~ Cod f
) => Functor' (obP :: i > Constraint)
(opP :: Hom i)
(p :: Hom i)
(obQ :: j > Constraint)
(opQ :: Hom j)
(q :: Hom j)
(f :: i > j) where
type Dom f :: Hom i
type Cod f :: Hom j
• Expected a type, but ‘j’ has kind ‘k’
• In the first argument of ‘Hom’, namely ‘j’
In the kind ‘Hom j’

34  type Cod f :: Hom j
 ^
The only way I can find to make this one compile is to make i
and j
explicit parameters with explicit kinds:
class ( obP ~ Ob p
, opP ~ Dom p
, obQ ~ Ob q
, opQ ~ Dom q
, p ~ Dom f
, q ~ Cod f
) => Functor' (i :: Type)
(j :: Type)
(obP :: i > Constraint)
(opP :: Hom i)
(p :: Hom i)
(obQ :: j > Constraint)
(opQ :: Hom j)
(q :: Hom j)
(f :: i > j) where
type Dom f :: Hom i
type Cod f :: Hom j
Trac field  Value 

Version  8.5 
Type  Bug 
TypeOfFailure  OtherFailure 
Priority  normal 
Resolution  Unresolved 
Component  Compiler (Type checker) 
Test case  
Differential revisions  
BlockedBy  
Related  
Blocking  
CC  
Operating system  
Architecture 
Edit: Everything I wrote in this comment was really stupid. Sorry, ignore it!
Yes, that's what I want, though I wonder if there may be other ways to achieve the same effect, without actually implementing the described translation.
I'll try and write out a better example of how it might be useful, and experiment with how painful it is to do the transformation manually.
Edit: Everything else I had originally written in this comment was dumb. Sorry, ignore it!
The following code fails to compile:
{# 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 toplevel instances:
instance C [a] Int where ...
baz :: [a] > String
baz = show . foo
Or to give the simpler example, this does too:
wibble :: forall a b fb c. (a, fb ~ F b, a => fb, a => c) => Dict (F b, c)
wibble = Dict
This demonstrates there's no shadowing (it compiles):
liftOb :: forall f cod other a.
( Functor f, cod ~ Cod f, Ob (Dom f) a
, forall a. Ob (Dom f) a => Ob cod (f a)
, forall a. Ob (Dom f) a => Ob other (f a)
) => Dict (Ob cod (f a), Ob other (f a))
liftOb = Dict
Not if the variable is a skolem (is that the right terminology?), which is what I intended. I should have been clearer.