Skip to content

No instance for Typeable with promoted GADT containing type family

Summary

I've been experimenting with promoted GADTs and I had trouble because some function I was applying needed a Typeable instance, and to my surprise, there wasn't one, though GHC is supposed to produce and instance for every type. In this case it seems to be related to the fact that there's a type family in the type definition.

Steps to reproduce

cabal run this sample program:

#!/usr/bin/env cabal
{- cabal:
  default-language: GHC2021
  build-depends:
    base
-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeData #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fprint-explicit-coercions #-}

import Data.Typeable (typeOf)

type data DayOfWeekK = SundayT | MondayT | TuesdayT

type data DaySubset = AnyDay | Weekend

data DayOfWeek_ (daySubset :: DaySubset) (b :: Bool) where
  Sunday :: DayOfWeek_ a (Supports a SundayT)
  Monday :: DayOfWeek_ a (Supports a MondayT)
  Tuesday :: DayOfWeek_ a (Supports a TuesdayT)

type DayOfWeek a = DayOfWeek_ a True

type family Supports (daySubset :: DaySubset) (dayOfWeek :: DayOfWeekK) :: Bool where
  Supports AnyDay _ = True
  Supports Weekend SundayT = True
  Supports _ _ = False

newtype Tagged a b = Tagged b

type Count (daySubset :: DaySubset) (dayOfWeek :: DayOfWeek daySubset) = Tagged '("Count", daySubset, dayOfWeek) Int

main :: IO ()
main = print $ typeOf (undefined :: Count Weekend Sunday)

This produces the error:

/Users/lkopnicky/gadt_refinement/no_typeable_demo.hs:36:16: error: [GHC-39999]
    • No instance for ‘ghc-internal-9.1001.0:GHC.Internal.Data.Typeable.Internal.Typeable
                         (Sunday |> (DayOfWeek_ <Weekend>_N (Main.D:R:Supports[1]))_N)’
        arising from a use of ‘typeOf’
    • In the second argument of ‘($)’, namely
        ‘typeOf (undefined :: Count Weekend Sunday)’
      In the expression:
        print $ typeOf (undefined :: Count Weekend Sunday)
      In an equation for ‘main’:
          main = print $ typeOf (undefined :: Count Weekend Sunday)
   |
36 | main = print $ typeOf (undefined :: Count Weekend Sunday)
   |                ^^^^^^

Expected behavior

What do you expect the reproducer described above to do?

Print out a type representation. Typeable is supposed to be automatically derived by the compiler for every type.

Environment

  • GHC version used: 9.10.1

Optional:

  • Operating System: macOS 14.6.1
  • System Architecture: aarch64
Edited by Lyle Kopnicky
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information