#12239 closed bug (duplicate)

Dependent type family does not reduce

Reported by: int-index Owned by: goldfire
Priority: high Milestone: 8.2.1
Component: Compiler (Type checker) Version: 8.0.1
Keywords: TypeInType, TypeFamilies Cc: goldfire, qnikst
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #11348, #12088 Differential Rev(s):
Wiki Page:

Description

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’

Change History (11)

comment:1 Changed 13 months ago by int-index

Cc: goldfire added

comment:2 Changed 13 months ago by qnikst

Cc: qnikst added

comment:3 Changed 13 months ago by goldfire

Owner: set to goldfire

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

comment:4 Changed 13 months ago 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?

comment:5 Changed 13 months ago by goldfire

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

comment:6 Changed 11 months ago by int-index

Milestone: 8.2.1
Priority: normalhigh

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

comment:7 Changed 11 months ago 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-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.

comment:8 Changed 11 months ago 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 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)?

comment:9 Changed 11 months ago by mpickering

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.

comment:10 Changed 11 months ago by mpickering

In fact, also intimately related to #12088

comment:11 Changed 11 months ago by int-index

Resolution: duplicate
Status: newclosed
Note: See TracTickets for help on using tickets.