Dependent type family does not reduce

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’

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

mentioned in issue #12088 (closed)

changed weight to 5

added Tbug Trac import typechecker labels

assigned to @rae

I was wondering if someone would find a way to tickle this. I'm pretty sure you've hit the shortcoming detailed here.

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?

Yes, that's what I meant. Perhaps it would have been clearer if I said "I was wondering...".

changed milestone to %8.2.1

changed weight to 7

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).

Trac metadata

Trac field	Value
Priority	normal → high

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-TcTyVars -- 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.

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 ForAllTys arise, but the Kinds in TyVarBinders 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)?

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 (closed).

Trac metadata

Trac field	Value
Related	- → #11348 (closed)

In fact, also intimately related to #12088 (closed)

Trac metadata

Trac field	Value
Related	#11348 (closed) → #11348 (closed), #12088 (closed)

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedDuplicate

added TypeFamilies TypeInType labels

added Phigh label