Haskell type family applications are not evaluated

9
votes

I found an interesting situation, when using data kinds with type families.

The compiler's error message is No instance for (C (ID ())) arising from a use of W. It suggests that a type family application is not fully evaluated, even when it is saturated. :kind! ID () evaluates to (), so according to the C () instance should be used.

{-# LANGUAGE GADTs, TypeFamilies, UndecidableInstances, FlexibleContexts #-}

type family ID t where
  ID t = t

class C t where
instance C () where

data W where
  W :: C (AppID t) => P t -> W

type family AppID t where
  AppID t = (ConstID t) ()

type family ConstID t where
  ConstID t = ID

data P t where
  P :: P t

data A

w :: W
w = W (P :: P A)

Could I somehow force the evaluation of ID ()? Is it a compiler bug?

I'm using GHC 7.8.3

1
haskellgadttype-familiesdata-kinds
How does (ID ()) evaluate to anything? There are no instances for the ID family. – augustss
I wrote it as a closed type family (haskell.org/haskellwiki/GHC/…) – Boldizsár Németh
Writing it as a normal type family does not change the error. – Boldizsár Németh
Sorry, I didn't read your code carefully enough. Yeah, it looks like it should work. – augustss
Eta-expanding ConstID t seems to work. Maybe there is some bug in the handling of partially applied type families as in ID. (Honestly, I thought these were disallowed. Did we effectively get type-level lambdas lately?) – chi

1 Answers

2
votes

The problem is the kind of ConstID.

type family ConstID t a where
  ConstID t a = ID a