Don't infer kind family applications in type patterns

[goldfirere]

When I say

{-# LANGUAGE GADTs, TypeFamilies, TypeOperators, DataKinds, PolyKinds,
             UndecidableInstances #-}

module Illegal where

import GHC.Exts ( Any )

data Elem :: [a] -> a -> * where
  EZ :: Elem (x ': xs) x
  ES :: Elem xs x -> Elem (y ': xs) x

infixr 5 ++
type family xs ++ ys where
  '[]       ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)

data LengthEv :: [a] -> * where
  LEZ :: LengthEv '[]
  LES :: LengthEv xs -> LengthEv (x ': xs)

type family ShiftElem (l :: LengthEv xs1) (e :: Elem (xs1 ++ xs2) x) :: Elem (xs1 ++ y ': xs2) x where
  ShiftElem ('LES l) 'EZ = Any

{-
Elem :: forall (a :: *). [a] -> a -> *
EZ :: forall (a :: *) (list :: [a]) (elt :: a).
      forall (xs :: [a]).
      (list ~ (elt ': xs)) => Elem list elt

(++) :: forall (k :: *). [k] -> [k] -> *

LengthEv :: forall (a :: *). [a] -> *
LES :: forall (a :: *) (list :: [a]).
       forall (x :: a) (xs :: [a]).
       (list ~ (x ': xs)) => LengthEv a xs -> LengthEv a list

ShiftElem :: forall (a :: *) (xs1 :: [a]) (xs2 :: [a]) (x :: a) (y :: a).
             LengthEv a xs1 -> Elem a (xs1 ++ xs2) x
          -> Elem a (xs1 ++ y ': xs2) x

axSE :: forall (a :: *) (xs1 :: [a]) (l :: LengthEv a xs1) (x :: a) (xs2 :: [a])
               (y :: a) (c1 :: (x ': xs1) ~ (x ': xs1)) (tail :: [a])
               (c2 :: (x ': tail) ~ (x ': tail))
               (c3 :: Elem a (x ': tail) x ~ Elem a ((x ': xs1) ++ xs2) x).
        ShiftElem a (x ': xs1) xs2 x y (LES a (x ': xs1) x xs1 c1 l)
                  (EZ a (x ': tail) x tail c2 |> c3)
        ~
        EZ a ((x ': xs1) ++ (y ': xs2)) x (xs1 ++ y ': xs2) co
  where
    co :: ((x ': xs1) ++ (y ': xs2)) ~ (x ': (xs1 ++ y ': xs2))
    co = ax++...


unrearranged:

axSE :: forall (a :: *) (xs1 :: [a]) (l :: LengthEv a xs1) (x :: a) (xs2 :: [a])
               (y :: a) (c1 :: (x ': xs1) ~ (x ': xs1))
               (c2 :: (x ': (xs1 ++ xs2)) ~ (x ': (xs1 ++ xs2)))
               (c3 :: Elem a (x ': (xs1 ++ xs2)) x ~ Elem a ((x ': xs1) ++ xs2) x).
        ShiftElem a (x ': xs1) xs2 x y (LES a (x ': xs1) x xs1 c1 l)
                  (EZ a (x ': (xs1 ++ xs2)) x (xs1 ++ xs2) c2 |> c3)
-}

I get

Illegal.hs:22:3:
    Illegal type synonym family application in instance: 'EZ
    In the equations for closed type family ‘ShiftElem’
    In the type family declaration for ‘ShiftElem’

Solution: invent a new flavor of metavariable that stubbornly refuses to unify with a type family. Also, make sure to abstract out coercions in type family patterns.

[RafaelBocquet]

Here is (maybe) another instance of the same issue :

module A where

import Prelude ()
import qualified Prelude as P

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

data CY (a :: *) (b :: a) (c :: TyFun' a *)
type instance (@@) (CY a b) c = *
data CX (a :: *) (b :: TyFun' a *)
type instance (@@) (CX a) b = TyPi a (CY a b)
$(P.return [])
data DG (a :: *) (b :: TyPi a (CX a)) (c :: a) (d :: a) (e :: TyFun' (b @@@ d @@@ c) *)
$(P.return [])
type instance (@@) (DG a b c d) e = ()

OUT.hs:29:15:
    Illegal type synonym family application in instance:
      (b @@@ d) @@@ c
    In the type instance declaration for ‘@@’

This prevents me from extracting some types when arguments have function types.

[goldfirere]

I do believe your code is an instance of this issue. Generally, using any type family in the declared kind of another type family will tickle this. I'm afraid this one isn't so quick to fix, having already looked into it and been blocked myself. I can prioritize this after July 10 (the POPL deadline), but I don't think I can look into it before then, as the POPL paper still needs lots of work.