#14131: Difference between newtype and newtype instance -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #7938, #9574, | Differential Rev(s): Phab:D3872 #13985 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
It's also worth noting that ​Phab:D3872 reverses a design decision made in #7938 and #9574 to only allow kind variables in the RHSes of associated type instances if they're explicitly bound by LHS type patterns.
But really, the a is Maybe a is bound by the often-neglected RHS type
I don't think it reverses it. We just didn't implement it properly. If we wrote out the kind arguments we'd see {{{ class C k where data family Nat @k :: k -> k -> Type instance C (k -> Type) where newtype Nat @(k -> Type) :: (k -> Type) -> (k -> Type) -> Type where Nat :: forall k (f::k->Type) (g::k->Type). (forall xx. f xx -> g xx) -> Nat @(k->Type) f g }}} So that `k` certainly is bound on the left, in the (invisible) kind pattern. pattern. I don't like this language. There is no "RHS type pattern". Rather, there are invisible kind patterns on the LHS. And this matters! Consider {{{ type family T (a :: Type) :: Type type family F :: k type instance T Int = Proxy (F :: k) }}} Now `T` does not have a kind parameter, and that `k` on the RHS of the `type instance` really is unbound. Writing out the kind arguments: {{{ type instance T Int = Proxy @k (F @k) }}} which is manifestly wrong. '''Bottom line''': we can't distinguish the two cases in the renamer. We have to check this in the type checker. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14131#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler