#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Oh dear, there are lots of thigs wrong here. I looked at {{{ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class C (a :: Type) (b :: k) where type T b }}} * First, `C` has a CUSK. But does `T`? Well `hsCeclHasCusk` reports True for the class decl, without even looking at `T`. This seems wrong. * `C` has a CUSK, but in `class C (a :: Type) (b :: k)`, I'm not sore how we get to know that `k :: Type`. Yet, without that `C` would not ahve a CUSK. * `getInitialKinds` returns this very bogus kind for `T`: {{{ kcTyClGroup: initial kinds C :: forall k. * -> k -> Constraint T :: forall (k :: k_aWH[tau:1]) (co :: k_aWH[tau:1] GHC.Prim.~# *). (k |> {co_aWL}) -> * }}} * What is that `co` binder? It's created in the mysterious `kcLHsQTyVars` function, which does something very like `quantifyTyVars`, but by steam. It uses `tyCoVarsOfTypeWellScoped`, but neglects to filter out coercion variables; hence the bugos quantification over `co_aWL`. ------------------ I'm reluctant to reach for a quick fix here. It all looks very dodgy to me. The `getInitialKinds` function, which is the bit misbehaving here, should be very simple: * For CUSKs, the idea is that it's a ''complete, user-specified kind'', just like a top-level type signature for a term variable. II expect to do something very akin to `tcHsSigType`: that is, type-check the kind, solve any constraints that arise, and kind-generalise the result. It's made a bit trickier by the fact that instead of a `LHsSigType` like `forall a. a->a` we have some `LHsQTyVars` like `data T (a :: k) (b :: *)`. But it's basically all one kind signature, pretty much the same as `forall (a::k) (b::*). blah` * For non-CUSKs, we can safely simply make `T :: kappa`, without looking at the declaration at all! We can perhaps save ourselves a bit of fruitless unification by seeing that if its `data T (a :: ...) (b :: ...)` then we can make `T :: kappa1 -> kappa2 -> *`. But we don't have to look into those "..." parts; that's going to happen later. No `solveEqualities` for non-CUSKs. * Associated types should not be allowed to mess things up! They must be treated as CUSK-ish only if they are in fact complete. Fundamentally, the same rules should apply: every type variable should be annotated. But maybe we can make an exception for variables from the parent class, if the parent class has a CUSK. Eg {{{ class C (a :: *) where type F a (b :: * -> *) :: * }}} Here perhaps we can allow `a` not to be annotated in `F`'s defn because it comes from `C` which itself has a CUSK. The present code does not do this, and it's buggy as this ticket shows. Let's discuss. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler