type family applications in kinds are not (always) reduced

[RafaelBocquet]

Encountered this compilation error when trying to do defunctionalisation of dependently kinded type level functions :

{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, GADTs, TypeOperators,
             ScopedTypeVariables, TemplateHaskell, FlexibleInstances,
             ConstraintKinds, UndecidableInstances, TemplateHaskell #-}

module A where

data TyArr (a :: *) (b :: *) :: *
type family (a :: TyArr k1 k2 -> *) @@ (b :: k1) :: k2

data TyPi (a :: *) (b :: TyArr a * -> *) :: *
type family (a :: TyPi k1 k2 -> *) @@@ (b :: k1) :: k2 @@ b

data A (x :: TyArr Bool *) :: *
type instance A @@ 'False = ()
type instance A @@ 'True  = ((), ())

data B (x :: TyPi Bool A) :: *
type instance B @@@ 'False = '()
type instance B @@@ 'True  = '( '(), '())

A.hs:18:30:
    Expected kind ‘A @@ 'False’, but ‘'()’ has kind ‘()’
    In the type ‘()’
    In the type instance declaration for ‘@@@’

A.hs:18:30:
    Expected kind ‘A @@ 'False’, but ‘'()’ has kind ‘()’
    In the type ‘()’
    In the type instance declaration for ‘@@@’

A.hs:19:30:
    Expected kind ‘A @@ 'True’, but ‘'('(), '())’ has kind ‘((), ())’
    In the type ‘'((), ())’
    In the type instance declaration for ‘@@@’

A.hs:19:30:
    Expected kind ‘A @@ 'True’, but ‘'('(), '())’ has kind ‘((), ())’
    In the type ‘'((), ())’
    In the type instance declaration for ‘@@@’

It compiles fine with a $(return []) line inserted between the declarations for A and B.

[goldfirere]

Thanks for reporting.

Currently, GHC (including my branch) defers typechecking all instance declarations until after other type-level declarations are done. Even within instance-declaration checking, it doesn't bring already-checked instances into scope until all instances are checked. So I'm not surprised this fails.

This obviously has to be refined before releasing, but it shouldn't be hard for GHC to guess that it needs the instances for A before working on the instances for B, given that A appears in a kind in the declaration for B. If two type families' instances need to be checked in an interleaved manner, that would be hard to figure out, but I'll save that until someone can demonstrate a compelling use case.

Another workaround (that won't work for you here, I think) is to use a closed type family. Because there are no instances there, the path through GHC is different and closed families end up "in scope" sooner than instances. In the final release, this distinction between open and closed families will not be noticeable.

[RafaelBocquet]

In this case, the instances should be in scope, yet there is a reduction issue (related to https://github.com/goldfirere/ghc/issues/18 ?).

data family Sing (k :: *) :: k -> *
type Sing' (x :: k) = Sing k x
data TyArr' (a :: *) (b :: *) :: *
type TyArr (a :: *) (b :: *) = TyArr' a b -> *
type family (a :: TyArr k1 k2) @@ (b :: k1) :: k2
data TyPi' (a :: *) (b :: TyArr a *) :: *
type TyPi (a :: *) (b :: TyArr a *) = TyPi' a b -> *
type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b
$(return [])
data T (a :: *) (b :: *) where
  T1 :: forall a. T a a
  T2 :: forall a b. T a b -> T a (b, b)

data A (a :: *) (x :: TyArr' * *)
$(return [])
data B (a :: *) (x :: TyPi' * (A a))
$(return [])
data C (x :: TyArr' * *)
$(return [])
data D (x :: TyPi' * C)
$(return [])
type instance A a @@ x  = *
$(return [])
type instance B a @@@ x = T a x
$(return [])
type instance C @@ a = TyPi * (A a)
$(return [])
type instance D @@@ a = B a 
$(return [])

data instance Sing (T a b) x where
  ST1 :: forall a. Sing (T a a) 'T1
  ST2 :: forall (a :: *) (b :: *) (c :: D @@@ a @@@ b). Sing (T a (b, b)) ('T2 c)

ghc: panic! (the 'impossible' happened)
  (GHC version 7.11.20150527 for x86_64-unknown-linux):
    ASSERT failed! file compiler/types/TyCoRep.hs, line 1817

Replacing D @@@ a @@@ b with its reduction T a b allows the code to compile.

[goldfirere]

Interesting. Probably not closely related to #18, despite the very similar error message. Thanks, as always, for posting.

Incidentally, if you're trying to do something interesting with my branch and a bug is holding you up, please do tell me. I'm working on other projects until mid-July. Then I have a bunch of refactoring that Simon suggested, and only then will I start addressing these issues, not until August at the earliest. So if you want a fix sooner, just ask.

[RafaelBocquet]

I'm working on code extraction from Coq to Haskell, preserving as much type information as possible. I'm currently trying to see if a translation without any unsafe casts is possible with your branch. I should probably take some time to get a basic understanding of System FC though.

I didn't get any really blocking bug before this one today (can you look into this one ?) :

module A where
data family Sing (k :: *) :: k -> *
type Sing' (x :: k) = Sing k x
data TyFun' (a :: *) (b :: *) :: *
type TyFun (a :: *) (b :: *) = TyFun' a b -> *
type family (a :: TyFun k1 k2) @@ (b :: k1) :: k2
data TyPi' (a :: *) (b :: TyFun a *) :: *
type TyPi (a :: *) (b :: TyFun a *) = TyPi' a b -> *
type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b
$(return [])

data A (a :: *) (b :: a) (c :: TyFun' a *)
type instance (@@) (A a b) c = *
$(return [])
data B (a :: *) (b :: TyFun' a *)
type instance (@@) (B a) b = TyPi a (A a b)
$(return [])
data C (a :: *) (b :: TyPi a (B a)) (c :: a) (d :: a) (e :: TyFun' (b @@@ c @@@ d) *)

gives with -ddump-tc-trace

      Expected a type, but
      ‘(@@@)
         k10
         ((A a |> <a>_R -> Sym cobox0) c)
         a
         ((@@@) a (B a) a b c |> Sub cobox1)
         d’ has kind
      ‘(@@) * a ((A a |> <a>_R -> Sym cobox0) c) d’
      In the first argument of ‘TyFun'’, namely ‘(b @@@ c) @@@ d’
      In the kind ‘TyFun' ((b @@@ c) @@@ d) *’

A a c @@ d should reduce to *. It seems the coercion prevents the type family application from being reduced ?

[goldfirere]

That's awesome to hear. Please let me know how it goes -- this is exactly the kind of stress-testing my branch needs.

In any case, this bug is now fixed. Thankfully, it was fairly easy.

If you're curious, it wasn't the coercion blocking the type family reduction, although I spent a while looking at that very obvious-looking potential mistake. The real problem was the kind of @@@, which ended up looking like forall k1 (k2 :: ...) k1. .... Notice the two k1's. Anyway, once I found it, it was easy to fix.

[RafaelBocquet]

Thanks for the quick fix.

I put my current code in https://github.com/RafaelBocquet/haskell-extraction, the current output is in https://github.com/RafaelBocquet/haskell-extraction/blob/master/OUT.hs.

I should probably have created three issues as the first two bugs are not fixed. I didn't encounter a case in which either of these is blocking yet, but I expect I will.

[goldfirere]

The first issue (now #33) shouldn't become blocking, as the $(return []) trick should always fix. Do let me know if #34 starts holding you up.