{"action":"created","issue":{"url":"https://api.github.com/repos/goldfirere/ghc/issues/15","labels_url":"https://api.github.com/repos/goldfirere/ghc/issues/15/labels{/name}","comments_url":"https://api.github.com/repos/goldfirere/ghc/issues/15/comments","events_url":"https://api.github.com/repos/goldfirere/ghc/issues/15/events","html_url":"https://github.com/goldfirere/ghc/issues/15","id":73996802,"number":15,"title":"Don't infer kind family applications in type patterns","user":{"login":"goldfirere","id":1958003,"avatar_url":"https://avatars.githubusercontent.com/u/1958003?v=3","gravatar_id":"","url":"https://api.github.com/users/goldfirere","html_url":"https://github.com/goldfirere","followers_url":"https://api.github.com/users/goldfirere/followers","following_url":"https://api.github.com/users/goldfirere/following{/other_user}","gists_url":"https://api.github.com/users/goldfirere/gists{/gist_id}","starred_url":"https://api.github.com/users/goldfirere/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/goldfirere/subscriptions","organizations_url":"https://api.github.com/users/goldfirere/orgs","repos_url":"https://api.github.com/users/goldfirere/repos","events_url":"https://api.github.com/users/goldfirere/events{/privacy}","received_events_url":"https://api.github.com/users/goldfirere/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-05-07T13:55:28Z","updated_at":"2015-06-23T13:05:31Z","closed_at":null,"body":"When I say\r\n\r\n```\r\n{-# LANGUAGE GADTs, TypeFamilies, TypeOperators, DataKinds, PolyKinds,\r\n             UndecidableInstances #-}\r\n\r\nmodule Illegal where\r\n\r\nimport GHC.Exts ( Any )\r\n\r\ndata Elem :: [a] -> a -> * where\r\n  EZ :: Elem (x ': xs) x\r\n  ES :: Elem xs x -> Elem (y ': xs) x\r\n\r\ninfixr 5 ++\r\ntype family xs ++ ys where\r\n  '[]       ++ ys = ys\r\n  (x ': xs) ++ ys = x ': (xs ++ ys)\r\n\r\ndata LengthEv :: [a] -> * where\r\n  LEZ :: LengthEv '[]\r\n  LES :: LengthEv xs -> LengthEv (x ': xs)\r\n\r\ntype family ShiftElem (l :: LengthEv xs1) (e :: Elem (xs1 ++ xs2) x) :: Elem (xs1 ++ y ': xs2) x where\r\n  ShiftElem ('LES l) 'EZ = Any\r\n\r\n{-\r\nElem :: forall (a :: *). [a] -> a -> *\r\nEZ :: forall (a :: *) (list :: [a]) (elt :: a).\r\n      forall (xs :: [a]).\r\n      (list ~ (elt ': xs)) => Elem list elt\r\n\r\n(++) :: forall (k :: *). [k] -> [k] -> *\r\n\r\nLengthEv :: forall (a :: *). [a] -> *\r\nLES :: forall (a :: *) (list :: [a]).\r\n       forall (x :: a) (xs :: [a]).\r\n       (list ~ (x ': xs)) => LengthEv a xs -> LengthEv a list\r\n\r\nShiftElem :: forall (a :: *) (xs1 :: [a]) (xs2 :: [a]) (x :: a) (y :: a).\r\n             LengthEv a xs1 -> Elem a (xs1 ++ xs2) x\r\n          -> Elem a (xs1 ++ y ': xs2) x\r\n\r\naxSE :: forall (a :: *) (xs1 :: [a]) (l :: LengthEv a xs1) (x :: a) (xs2 :: [a])\r\n               (y :: a) (c1 :: (x ': xs1) ~ (x ': xs1)) (tail :: [a])\r\n               (c2 :: (x ': tail) ~ (x ': tail))\r\n               (c3 :: Elem a (x ': tail) x ~ Elem a ((x ': xs1) ++ xs2) x).\r\n        ShiftElem a (x ': xs1) xs2 x y (LES a (x ': xs1) x xs1 c1 l)\r\n                  (EZ a (x ': tail) x tail c2 |> c3)\r\n        ~\r\n        EZ a ((x ': xs1) ++ (y ': xs2)) x (xs1 ++ y ': xs2) co\r\n  where\r\n    co :: ((x ': xs1) ++ (y ': xs2)) ~ (x ': (xs1 ++ y ': xs2))\r\n    co = ax++...\r\n\r\n\r\nunrearranged:\r\n\r\naxSE :: forall (a :: *) (xs1 :: [a]) (l :: LengthEv a xs1) (x :: a) (xs2 :: [a])\r\n               (y :: a) (c1 :: (x ': xs1) ~ (x ': xs1))\r\n               (c2 :: (x ': (xs1 ++ xs2)) ~ (x ': (xs1 ++ xs2)))\r\n               (c3 :: Elem a (x ': (xs1 ++ xs2)) x ~ Elem a ((x ': xs1) ++ xs2) x).\r\n        ShiftElem a (x ': xs1) xs2 x y (LES a (x ': xs1) x xs1 c1 l)\r\n                  (EZ a (x ': (xs1 ++ xs2)) x (xs1 ++ xs2) c2 |> c3)\r\n-}\r\n```\r\nI get\r\n```\r\nIllegal.hs:22:3:\r\n    Illegal type synonym family application in instance: 'EZ\r\n    In the equations for closed type family ‘ShiftElem’\r\n    In the type family declaration for ‘ShiftElem’\r\n```\r\n\r\nSolution: 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."},"comment":{"url":"https://api.github.com/repos/goldfirere/ghc/issues/comments/114493950","html_url":"https://github.com/goldfirere/ghc/issues/15#issuecomment-114493950","issue_url":"https://api.github.com/repos/goldfirere/ghc/issues/15","id":114493950,"user":{"login":"goldfirere","id":1958003,"avatar_url":"https://avatars.githubusercontent.com/u/1958003?v=3","gravatar_id":"","url":"https://api.github.com/users/goldfirere","html_url":"https://github.com/goldfirere","followers_url":"https://api.github.com/users/goldfirere/followers","following_url":"https://api.github.com/users/goldfirere/following{/other_user}","gists_url":"https://api.github.com/users/goldfirere/gists{/gist_id}","starred_url":"https://api.github.com/users/goldfirere/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/goldfirere/subscriptions","organizations_url":"https://api.github.com/users/goldfirere/orgs","repos_url":"https://api.github.com/users/goldfirere/repos","events_url":"https://api.github.com/users/goldfirere/events{/privacy}","received_events_url":"https://api.github.com/users/goldfirere/received_events","type":"User","site_admin":false},"created_at":"2015-06-23T13:05:31Z","updated_at":"2015-06-23T13:05:31Z","body":"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."}}