#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: closed Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: fixed | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: indexed- crash or panic | types/should_compile/T15142 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I agree with everything in that Note. Why have the explicit `forall`? Because perhaps the user wants inference, not CUSKness. By making a decision based on the `forall`, then the user can get what they want. For example: {{{#!hs data T1 :: k1 k2 -> Type where MkT1 :: forall (k1 :: Type -> Type) (k2 :: Type) (x :: k1 k2). T1 x }}} There are two possible meanings for this. Meaning 1 (M1): {{{#!hs T1 :: forall (k1 :: Type -> Type) (k2 :: Type). k1 k2 -> Type MkT1 :: forall (k1 :: Type -> Type) (k2 :: Type) (x :: k1 k2). T1 k1 k2 x }}} Meaning 2 (M2): {{{#!hs T1 :: forall (k :: Type) (k1 :: k -> Type) (k2 :: k). k1 k2 -> Type MkT1 :: forall (k :: Type) (k1 :: k -> Type) (k2 :: k) (x :: k1 k2). (k ~# Type) -> T1 k k1 k2 x }}} In M1, we do not quantify `T1`'s kind further, and the data constructor is not GADT-like. In M2, though, we ''do'' generalize, making `MkT1` a GADT constructor packing an equality. M1 is what happens if `T1` does not have a CUSK. `M2` is what happens when it does. Having CUSKness depend on the presence of the `forall` allows users to choose which of these interpretations to use. We ''could'' absolutely, remove it, but then I don't know how to write `T1` with meaning M1. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler