Skip to content

Surprising type (family) type derived

Consider the following module

{-# LANGUAGE TypeFamilies #-}
module Bug5 where

class C a where
    type T a
    f :: T a -> T a -> T a

data D a = D { t :: T a }

g r = f (t r) (t r)

Now ask for the type of g

*Bug5> :t g
g :: (T a ~ T a1, C a1) => D a -> T a1

Why isn't the type

g :: (C a) => D a -> T a

?

The strange type is a minor nuisance, but it gets worse

{-# LANGUAGE TypeFamilies #-}
module Bug6 where

class C a where
    type T a
    type U a
    f :: T a -> T a -> T a
    x :: U a -> T a

data D a = D { t :: T a, u :: U a }

g r = f (t r) (x (u r))

This doesn't type check at all.

An even simpler example that fails:

{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
module Bug7 where

class C a where
    type T a
    type U a
    x :: U a -> T a

data D a = D (U a)

g :: (C a) => D a -> T a
g (D u) = x u
Trac metadata
Trac field Value
Version 6.10.1
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC lennart@augustsson.net
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information