Opened 4 months ago
Last modified 3 weeks ago
#14451 new bug
Need proper SCC analysis of type declarations, taking account of CUSKs
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.2.1 |
Keywords: | TypeInType | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
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 (5)
comment:1 Changed 4 months ago by
comment:2 Changed 4 months ago by
Keywords: | TypeInType added |
---|
Yes, this could be #11203, but I haven't done enough analysis to be sure.
comment:3 Changed 4 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 6 weeks 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 3 weeks ago by
Wiki Page: | → https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference |
---|
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.