[GHC] #12239: Dependent type family does not reduce
#12239: Dependent type family does not reduce -------------------------------------+------------------------------------- Reporter: int-index | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: TypeInType, | Operating System: Unknown/Multiple TypeFamilies | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- When a type family is used in a kind of an argument for another type family, it does not reduce. Here's example code: {{{ {-# LANGUAGE TypeInType, GADTs, TypeFamilies #-} import Data.Kind (Type) data N = Z | S N data Fin :: N -> Type where FZ :: Fin (S n) FS :: Fin n -> Fin (S n) type family FieldCount (t :: Type) :: N type family FieldType (t :: Type) (i :: Fin (FieldCount t)) :: Type data T type instance FieldCount T = S (S (S Z)) type instance FieldType T FZ = Int type instance FieldType T (FS FZ) = Bool type instance FieldType T (FS (FS FZ)) = String }}} Unfortunately, I get these errors during typechecking: {{{ [1 of 1] Compiling Main ( fieldtype.hs, fieldtype.o ) fieldtype.hs:19:27: error: • Expected kind ‘Fin (FieldCount T)’, but ‘'FZ’ has kind ‘Fin ('S n0)’ • In the second argument of ‘FieldType’, namely ‘FZ’ In the type instance declaration for ‘FieldType’ fieldtype.hs:20:28: error: • Expected kind ‘Fin (FieldCount T)’, but ‘'FS 'FZ’ has kind ‘Fin ('S ('S n0))’ • In the second argument of ‘FieldType’, namely ‘FS FZ’ In the type instance declaration for ‘FieldType’ fieldtype.hs:21:28: error: • Expected kind ‘Fin (FieldCount T)’, but ‘'FS ('FS 'FZ)’ has kind ‘Fin ('S ('S ('S n0)))’ • In the second argument of ‘FieldType’, namely ‘FS (FS FZ)’ In the type instance declaration for ‘FieldType’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12239 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12239: Dependent type family does not reduce -------------------------------------+------------------------------------- Reporter: int-index | Owner: Type: bug | Status: new Priority: normal | Milestone: 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 int-index): * cc: goldfire (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12239#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12239: Dependent type family does not reduce -------------------------------------+------------------------------------- Reporter: int-index | Owner: Type: bug | Status: new Priority: normal | Milestone: 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 qnikst): * cc: qnikst (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12239#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12239: Dependent type family does not reduce -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 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): * owner: => goldfire Comment: I was wondering if someone would find a way to tickle this. I'm pretty sure you've hit the shortcoming detailed [https://github.com/ghc/ghc/blob/e368f3265b80aeb337fbac3f6a70ee54ab14edfd/com... here]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12239#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12239: Dependent type family does not reduce -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 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 simonpj):
I was wondering if someone would find a way to tickle this
I don't understand what you mean, Richard. The code in the Description *does* tickle it, no? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12239#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12239: Dependent type family does not reduce -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 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): Yes, that's what I meant. Perhaps it would have been clearer if I said "I ''was'' wondering...". -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12239#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12239: Dependent type family does not reduce -------------------------------------+------------------------------------- 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 int-index): * priority: normal => high * milestone: => 8.2.1 Comment: I'm raising the priority and setting the milestone to 8.2 since 8.2 is a consolidation release and I would love to see the bug fixed. Tried to fix it myself but after a few hours of reading GHC source I realized that I lack the necessary expertise (although I could try again if someone was to mentor me). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12239#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12239: Dependent type family does not reduce -------------------------------------+------------------------------------- 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): This is annoying to fix but I don't think will require any great engineering feats. The be clear, the problem is to convert a type `forall (a :: F x). blah` to `forall (b :: s). blah[a |-> b |> co]`, where `s` is the flattened form of `F x` (either an fuv or some other type) and `co :: s ~ F x`. Here's the approach I have in mind: include a `TCvSubst` in `FlattenEnv`. Whenever the kind of a bound type variable is flattened, extend the substitution to map the original variable (that is, `a`) to a new one `b` (with a fresh unique -- use `uniqAway`) that has the flattened kind (and is casted, as above). This substitution must be applied over the entire scope of the bound variable (the `blah` in our example). But it would be inefficient just to apply the substitution, so we consult this substitution in `flattenTyVar` as appropriate. Specifically, I think we would need to update the first case in `flatten_tyvar1`, which deals with non-`TcTyVar`s -- that is, locally bound variables. Does this sound like something you might tackle? I'm sure bumps will come up along the road, but if you're feeling like getting your hands dirty here, I can continue to advise. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12239#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12239: Dependent type family does not reduce -------------------------------------+------------------------------------- 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 int-index):
Does this sound like something you might tackle?
Yes. Your explanation is very helpful.
I'm sure bumps will come up along the road, but if you're feeling like getting your hands dirty here, I can continue to advise.
Thank you. So, my understanding is that during type checking `ForAllTy`s arise, but the `Kind`s in `TyVarBinder`s don't get flattened, hence the error. However, once I added a `traceFlat` to the beginning of `flatten_one` clause for `ForAllTy` it didn't show up in the compilation logs (adding it in other clauses worked, so I assume that I added it correctly). Therefore I conclude that control flow doesn't reach this part of the code and no changes will affect the result of compilation. (1) What other parts of code should be changed and how, before I can start fixing `flatten_one` for `ForAllTy`? (2) Where exactly those `ForAllTy` get inserted in the example code (in the ticket description)? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12239#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12239: Dependent type family does not reduce -------------------------------------+------------------------------------- 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: #11348 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * related: => #11348 Comment: Int-index and I have been working through this together this afternoon and it is nothing to do with what Richard initially expected. Instead, the problem is that whilst checking the kind of the argument to `FieldType`, we need knowledge of the instances of `FieldCount` which only get added to the environment *after* all the type family instances have been type checked. So instead this ticket is related to #11348. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12239#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12239: Dependent type family does not reduce -------------------------------------+------------------------------------- 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: #11348, #12088 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * related: #11348 => #11348, #12088 Comment: In fact, also intimately related to #12088 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12239#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12239: Dependent type family does not reduce -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: closed Priority: high | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeInType, Resolution: duplicate | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #11348, #12088 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by int-index): * status: new => closed * resolution: => duplicate -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12239#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC