#12564: Type family in type pattern kind -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * priority: normal => high -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12564#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12564: Type family in type pattern kind -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): ummm... Maybe :) In reality, probably not. It depends on how my levity polymorphism stuff evolves. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12564#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12564: Type family in type pattern kind -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.2.1 => 8.4.1 Comment: In that case I'll bump this off to 8.4. Do feel free to bump it back if things change, however. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12564#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12564: Type family in type pattern kind -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: 14119 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I've made a new ticket #14119 discussing a refactoring of type patterns. That ticket would solve this one. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12564#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12564: Type family in type pattern kind -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: 14119 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I have an approach here worth documenting. In brief: flatten equations' left-hand sides, emitting constraints during reduction. Here is how the example in the OP would work. Original equation: {{{#!hs At (x ': _) FZ = x }}} with implicit things made explicit: {{{#!hs At @a ((:) @a x _1) (FZ @(Len @a _1)) = x }}} But now, we ''flatten''. By this, I mean we take all type family applications on the LHS and convert them into variables, and assert equality constraints that the variables equal the original type family applications. To wit: {{{#!hs (m ~ Len @a _1) => At @a ((:) @a x _1) (FZ @m) = x }}} This yields a ''constrained'' type family equation. (Note: this is mostly unrelated to [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1075&context=compsci_pubs Constrained Type Families]) During reduction, this equation would match a target regardless of the (implicit) argument to `FZ`, but the matcher would then emit a constraint asserting that this argument equals `Len @a _1`. It's quite like how class instance matching works: we match against the head, emitting any instance constraints. Type family equations give rise to axioms in Core. To keep type safety, we would need these axioms to take the evidence of the equality match as arguments. Continuing our example, we would get this axiom: {{{ axAt :: forall (a :: Type) (x :: a) (_1 :: [a]) (m :: Nat). forall (cv :: m ~ Len @a _1). At @a ((:) @a x _1) (FZ @m) ~ x }}} Note that there are two `forall`s: the first binds type variables and the second binds coercion variables. In this case, the coercion variable `cv` is unused in the RHS, but it might potentially be mentioned. This equation could be used to reduce `At ["a", "b", "c"] FZ` to `"a"`. We would use the instantiated axiom {{{ axAt Symbol "a" ["b", "c"] 2 coLen :: At ["a", "b", "c"] FZ ~ "a" }}} where `coLen :: 2 ~ Len ["b", "c"]` is built from the axioms that describe the behavior of `Len`. Note that there is already some infrastructure for this: the `cvs` in `CoAxBranch` (and a few other places nearby) are exactly these coercion variables. What's remaining to do is to perform the flattening pass that inserts the cvs and to teach the type-family reduction mechanism (in `TcFlatten`) to emit the constraints. One challenge is that sometimes (`normaliseType`) we reduce type families without the ability to solve constraints, so some care must be taken there. However, these cases are outside our usual pipeline and can be special-cased. (While implementing `-XTypeInType`, I did this once upon a time, so I know it's possible.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12564#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12564: Type family in type pattern kind -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: 14119 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): * Bizarrely, I don't think we need to do much proving. The type safety proof depends on the non-overlap of axiom LHSs. That's unchanged here -- the overlap check must treat any type family application on an LHS just like it would a variable. The equality constraints serve only to reduce the applicability of axioms, never to increase it. Thus, no threats to safety. * But the evidence ''is'' used: it's passed to the coercion axiom. The evidence is the `coLen` in my example above. * I take back the "evidence may be mentioned" comment. * GHC passes loads of redundant information at every call site (e.g. `id @Bool True`). This is not new. The uniquely-determined check would help those other places too. I think, in the end, that idea is orthogonal to the plan here, which would work for `F x (G x) = True`, should we ever want to support that. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12564#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12564: Type family in type pattern kind -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: 14119 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): For anyone reading this ticket who is searching for a workaround: While I haven't found a general-purpose way to avoid this bug, in limited situations it's often possible to rewrite your type families in a way that shifts applications of type families from the left-hand side to the right- hand side. For example, GHC //does// accept this formulation of `At`: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} import Data.Kind import Data.Type.Equality data N = Z | S N type family Len (xs :: [a]) :: N where Len '[] = Z Len (_ ': xs) = S (Len xs) data Vec :: N -> Type -> Type where VNil :: Vec Z a (:>) :: a -> Vec n a -> Vec (S n) a type family ListToVec (l :: [a]) :: Vec (Len l) a where ListToVec '[] = VNil ListToVec (x:xs) = x :> ListToVec xs data Fin :: N -> Type where FZ :: Fin (S n) FS :: Fin n -> Fin (S n) type family At (xs :: [a]) (i :: Fin (Len xs)) :: a where At xs i = At' (ListToVec xs) i type family At' (xs :: Vec n a) (i :: Fin n) :: a where At' (x :> _) FZ = x At' (_ :> xs) (FS i) = At' xs i -- Unit tests test1 :: At '[True] FZ :~: True test1 = Refl test2 :: At [True, False] FZ :~: True test2 = Refl test3 :: At [True, False] (FS FZ) :~: False test3 = Refl }}} If you inspect the definition of `At`, you'll see why this works: {{{ λ> :info At type family At @a (xs :: [a]) (i :: Fin (Len @a xs)) :: a where forall a (xs :: [a]) (i :: Fin (Len @a xs)). At @a xs i = At' @(Len @a xs) @a (ListToVec @a xs) i }}} Note that the left-hand side, `At @a xs i`, does not contain any immediate uses of `Len`. (The kind of `i` does, but thankfully, GHC doesn't consider that to be an illegal type synonym family application.) The other uses of `Len` and `ListToVec` have been quarantined off on the right-hand side, where GHC can't complain about them. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12564#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12564: Type family in type pattern kind -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: 14119 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): After reading comment:13, I'm left wondering about how this idea would work in practice. I've wanted to define instances like these before: {{{#!hs type family Sing :: k -> Type type instance Sing @Type = TypeRep type instance Sing @(Sing a) = Sing }}} Currently, GHC prevents me from writing the `Sing @(Sing a)` instance since its argument mentions the `Sing` type family. If I understand the plan in comment:13, then GHC would turn this instance into something that looks roughly like this: {{{#!hs type instance (x ~ Sing a) => Sing @x = Sing }}} However, this might be a problem. We have both a `Sing @x` and a `Sing @Type` instance defined—wouldn't these instances conflict? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12564#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler