Opened 13 months ago
Closed 13 days ago
#14451 closed bug (fixed)
Need proper SCC analysis of type declarations, taking account of CUSKs
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.6.1 |
Component: | Compiler | Version: | 8.2.1 |
Keywords: | TypeInType, CUSKs | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | typecheck/should_compile/T14451 |
Blocked By: | Blocking: | ||
Related Tickets: | #7503 | Differential Rev(s): | |
Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference |
Description
{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs, RankNTypes, UndecidableInstances #-} import Data.Kind data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type type Cat ob = ob -> ob -> Type type family Apply (f :: a ~> b) (x :: a) :: b where Apply (CompSym2 f g) a = Comp f g a data CompSym2 :: (b ~> c) -> (a ~> b) -> (a ~> c) type a·b = Apply a b class Varpi (f :: i ~> j) where type Dom (f :: i ~> j) :: Cat i type Cod (f :: i ~> j) :: Cat j varpa :: Dom f a a' -> Cod f (f·a) (f·a') type family Comp (f::k1 ~> k) (g::k2 ~> k1) (a::k2) :: k where Comp f g a = f · (Apply g a)
This compiles, but if I replace the final line by
Comp f g a = f · (g · a)
oddly enough I get an error message about the method varpa
! Seemingly unrelated apart from using (·)
:
$ ghci2 hs/093-bug.hs GHCi, version 8.3.20170920: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( hs/093-bug.hs, interpreted ) hs/093-bug.hs:23:33: error: • Expected kind ‘i ~> i’, but ‘f’ has kind ‘i ~> j’ • In the first argument of ‘(·)’, namely ‘f’ In the second argument of ‘Cod’, namely ‘(f · a)’ In the type signature: varpa :: Dom f a a' -> Cod f (f · a) (f · a') | 23 | varpa :: Dom f a a' -> Cod f (f·a) (f·a') | ^ Failed, 0 modules loaded. Prelude>
NOW — let's randomly remove both lines that mention CompSym2
and it mysteriously works, again!
Apply
and (·)
seem to be equal up to variable names, I can't spot why
>> :set -fprint-explicit-foralls >> :set -fprint-explicit-kinds >> :set -fprint-explicit-coercions >> >> :kind Apply Apply :: forall {a} {b}. (a ~> b) -> a -> b >> :kind (·) (·) :: forall {a} {k}. (a ~> k) -> a -> k
but it works if I define (·)
as a type family rather than a synonym:
type family (f::a ~> b) · (x::a) :: b where f · x = Apply f x
so it's some difference between synonyms and TFs, but is it intentional? It's certainly odd how the error messages jumped the varpa
method when we actually modified Comp
.
Change History (9)
comment:1 Changed 13 months ago by
comment:2 Changed 13 months ago by
Keywords: | TypeInType added |
---|
Yes, this could be #11203, but I haven't done enough analysis to be sure.
comment:3 Changed 13 months ago by
I don't think this is #11203. Here's what I think is happening
Apply
,Comp
, andOO
(which I will use instead of the unicode dot symbol) are mutually
recursive, and so are kind-checked together.
- The first two have CUSKs and so
getInitialKinds
gives them polykinds, thuskcTyClGroup: initial kinds [r1 :-> ATcTyCon Apply :: forall a b. (a ~> b) -> a -> b, r2 :-> ATcTyCon Comp :: forall k1 k2 k. (k1 ~> k) -> (k2 ~> k1) -> k2 -> k, r4 :-> ATcTyCon OO :: k_aYg[tau:1] -> k_aYh[tau:1] -> k_aYi[tau:1]]
Good so far.
- But then pathetically, we run over all three declarations, gathering constraints
on the kind variables in
OO
. In the end we makeOO
insufficiently polymorphic, giving it kindOO :: forall b. (b ~> b) -> b -> b
whereas it should have kindOO :: forall a b. (a ~> b) -> a -> b
That's stupid:OO
's kind should obviously be the same asApply
's
What we should do is exactly what we do for value declarations:
- Take the SCC (the group of three declarations)
- Remove edges that point to type constructors that have a CUSK
- Do a new SCC on this thinned-out graph.
- Now
OO
will be first, in a SCC by itself, becauseApply
andComp
depend on it, but not vice versa (after removing those edges) - Now kind-check each smaller SCC one by one, generalising each in turn.
For bindings you can see the extra SCC analysis being done in TcBinds.tc_group
.
So all we have to do is to replicate this logic for types. Fiddly, perhaps, but not difficult.
comment:4 Changed 10 months ago by
Related Tickets: | → #7503 |
---|---|
Summary: | Type synonym of type family causes error, error jumps to (fairly) unrelated source location → Need proper SCC analysis of type declarations, taking account of CUSKs |
See also #7503
comment:5 Changed 10 months ago by
Wiki Page: | → https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference |
---|
comment:6 Changed 7 months ago by
Keywords: | CUSKs added |
---|
comment:7 Changed 2 weeks ago by
Amazingly, the original program in this ticket (including the Comp f g a = f · (g · a)
tweak):
{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs, RankNTypes, UndecidableInstances #-} import Data.Kind data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type type Cat ob = ob -> ob -> Type type family Apply (f :: a ~> b) (x :: a) :: b where Apply (CompSym2 f g) a = Comp f g a data CompSym2 :: (b ~> c) -> (a ~> b) -> (a ~> c) type a·b = Apply a b class Varpi (f :: i ~> j) where type Dom (f :: i ~> j) :: Cat i type Cod (f :: i ~> j) :: Cat j varpa :: Dom f a a' -> Cod f (f·a) (f·a') type family Comp (f::k1 ~> k) (g::k2 ~> k1) (a::k2) :: k where Comp f g a = f · (g · a)
Appears to have fixed itself at some point between GHC 8.4 and 8.6, since it typechecks on GHC 8.6.2 and HEAD. I'm not sure what commit caused that, but that's cool nonetheless.
Let me check to see if the same miracle happened to #7503.
comment:9 Changed 13 days ago by
Milestone: | → 8.6.1 |
---|---|
Resolution: | → fixed |
Status: | new → closed |
Test Case: | → typecheck/should_compile/T14451 |
Alas, #7503 was not entirely fixed—see https://ghc.haskell.org/trac/ghc/ticket/7503#comment:10. But this ticket is entirely fixed, so we can close this one now.
The error message thing is a red herring: the real culprit is lurking in this slightly minimized version of your program:
This appears to typecheck without issues. But there actually is an issue, if you poke around inside the file with GHCi:
Egad! Despite the fact that we've appeared to give
(·)
the kind(k1 ~> k2) -> k1 -> k2
, GHC somehow concludes that it actually has the more restrictive kind(k2 ~> k2) -> k2 -> k2
. (This, in turn, causes the strange error message you've observed.)As far as why this happens, my shot-in-the-dark guess is that this is a manifestation of #11203/#11453. But I'd need Richard to confirm this.