Weird kind inference problems with closed type families

Consider a problem of injective cons on a type-level list https://ghc.haskell.org/trac/ghc/ticket/12114. I made a small workaround by adding an intermediate data type List1 k. Here is my code:

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-}
{-# LANGUAGE KindSignatures, DataKinds, PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications     #-}
module TFTest where

import GHC.TypeLits
import Data.Proxy



-- | Synonym for a type-level snoc (injective!)
type (ns :: [k]) +: (n :: k) = GetList1 (SinkFirst (n ': ns))
infixl 5 +:



-- | A weird data type used to make `(+:)` operation injective.
--   `List k [k]` must have at least two elements.
data List1 k = L1Single k | L1Head k [k]

-- | Sink first element of a list to the end of the list
type family SinkFirst (xs :: [k]) = (ys :: List1 k) | ys -> xs where
  SinkFirst '[y]       = 'L1Single y
  -- SinkFirst (y ': x ': xs :: [Nat])
  --     = ('L1Head x (GetList1Nat (SinkFirst (y ': xs))) :: List1 Nat)
  SinkFirst (y ': x ': xs :: [k])
      = ('L1Head x (GetList1    (SinkFirst (y ': xs))) :: List1 k)

type family GetList1 (ts :: List1 k) = (rs :: [k]) | rs -> ts where
  GetList1 ('L1Single x) = '[x]
  GetList1 ('L1Head y (x ':xs)) = y ': x ': xs
type family GetList1Nat (ts :: List1 Nat) = (rs :: [Nat]) | rs -> ts where
  GetList1Nat ('L1Single x) = '[x]
  GetList1Nat ('L1Head y (x ': xs)) = y ': x ': xs

type family (++) (as :: [k]) (bs :: [k]) :: [k] where
  '[] ++ bs = bs
  (a ': as) ++ bs = a ': (as ++ bs)


ff :: Proxy k -> Proxy (as +: k) -> Proxy (k ': bs) -> Proxy (as ++ bs)
ff _ _ _ = Proxy

yy :: Proxy '[3,7,2]
yy = ff (Proxy @5) (Proxy @'[3,7,5]) (Proxy @'[5,2])

This gives me the following error:

~/TFTest.hs: 47, 21
• Couldn't match kind ‘k’ with ‘Nat’
  When matching the kind of ‘7 : xs’
  Expected type: Proxy ((3 : (7 : xs)) +: 5)
    Actual type: Proxy '[3, 7, 5]
• In the second argument of ‘ff’, namely ‘(Proxy @'[3, 7, 5])’
  In the expression:
    ff (Proxy @5) (Proxy @'[3, 7, 5]) (Proxy @'[5, 2])
  In an equation for ‘yy’:
      yy = ff (Proxy @5) (Proxy @'[3, 7, 5]) (Proxy @'[5, 2])

However, if I uncomment lines 26-27, the code works perfectly fine!

This behaviour feels like a bug in type checker, though I am not sure. If it is not, please, explain me what happens here? :)

Trac metadata

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