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 |