[GHC] #13538: Weird kind inference problems with closed type families

[GHC]

#13538: Weird kind inference problems with closed type families
-------------------------------------+-------------------------------------
           Reporter:  achirkin       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.2
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Incorrect
  Unknown/Multiple                   |  error/warning at compile-time
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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:
 {{{#!hs
 {-# 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? :)

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13538>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler