Elaborator really slow on types with lots of constructors

[locallycompact]

Hi, I'm trying to derive Show and Eq for a big type with approximately 200 constructors.

%language ElabReflection

data Key : Type where
  KC_NO : Key
  KC_TRANSPARENT : Key
  KC_A : Key
  KC_B : Key
  KC_C : Key
  KC_D : Key
  KC_E : Key
  KC_F : Key
  KC_G : Key
  KC_H : Key
  KC_I : Key
  KC_J : Key
  KC_K : Key
  KC_L : Key
  KC_M : Key
  KC_N : Key
  KC_O : Key
  KC_P : Key
  KC_Q : Key
  KC_R : Key
  KC_S : Key
  KC_T : Key
  KC_U : Key
  KC_V : Key
  KC_W : Key
  KC_X : Key
  KC_Y : Key
  KC_Z : Key
  KC_1 : Key
  KC_2 : Key
  KC_3 : Key
  KC_4 : Key
  KC_5 : Key
  KC_6 : Key
  KC_7 : Key
  KC_8 : Key
  KC_9 : Key
  KC_0 : Key
  KC_ENTER : Key
  KC_ESCAPE : Key
  KC_BACKSPACE : Key
  KC_TAB : Key
  KC_SPACE : Key
  KC_MINUS : Key
  KC_EQUAL : Key
  KC_LEFT_BRACKET : Key
  KC_RIGHT_BRACKET : Key
  KC_BACKSLASH : Key
  KC_NONUS_HASH : Key
  KC_SEMICOLON : Key
  KC_QUOTE : Key
  KC_GRAVE : Key
  KC_COMMA : Key
  KC_DOT : Key
  KC_SLASH : Key
  KC_CAPS_LOCK : Key
  KC_F1 : Key
  KC_F2 : Key
  KC_F3 : Key
  KC_F4 : Key
  KC_F5 : Key
  KC_F6 : Key
  KC_F7 : Key
  KC_F8 : Key
  KC_F9 : Key
  KC_F10 : Key
  KC_F11 : Key
  KC_F12 : Key
  KC_PRINT_SCREEN : Key
  KC_SCROLL_LOCK : Key
  KC_PAUSE : Key
  KC_INSERT : Key
  KC_HOME : Key
  KC_PAGE_UP : Key
  KC_DELETE : Key
  KC_END : Key
  KC_PAGE_DOWN : Key
  KC_RIGHT : Key
  KC_LEFT : Key
  KC_DOWN : Key
  KC_UP : Key
  KC_NUM_LOCK : Key
  KC_KP_SLASH : Key
  KC_KP_ASTERISK : Key
  KC_KP_MINUS : Key
  KC_KP_PLUS : Key
  KC_KP_ENTER : Key
  KC_KP_1 : Key
  KC_KP_2 : Key
  KC_KP_3 : Key
  KC_KP_4 : Key
  KC_KP_5 : Key
  KC_KP_6 : Key
  KC_KP_7 : Key
  KC_KP_8 : Key
  KC_KP_9 : Key
  KC_KP_0 : Key
  KC_KP_DOT : Key
  KC_NONUS_BACKSLASH : Key
  KC_APPLICATION : Key
  KC_KB_POWER : Key
  KC_KP_EQUAL : Key
  KC_F13 : Key
  KC_F14 : Key
  KC_F15 : Key
  KC_F16 : Key
  KC_F17 : Key
  KC_F18 : Key
  KC_F19 : Key
  KC_F20 : Key
  KC_F21 : Key
  KC_F22 : Key
  KC_F23 : Key
  KC_F24 : Key
  KC_EXECUTE : Key
  KC_HELP : Key
  KC_MENU : Key
  KC_SELECT : Key
  KC_STOP : Key
  KC_AGAIN : Key
  KC_UNDO : Key
  KC_CUT : Key
  KC_COPY : Key
  KC_PASTE : Key
  KC_FIND : Key
  KC_KB_MUTE : Key
  KC_KB_VOLUME_UP : Key
  KC_KB_VOLUME_DOWN : Key
  KC_LOCKING_CAPS_LOCK : Key
  KC_LOCKING_NUM_LOCK : Key
  KC_LOCKING_SCROLL_LOCK : Key
  KC_KP_COMMA : Key
  KC_KP_EQUAL_AS400 : Key
  KC_INTERNATIONAL_1 : Key
  KC_INTERNATIONAL_2 : Key
  KC_INTERNATIONAL_3 : Key
  KC_INTERNATIONAL_4 : Key
  KC_INTERNATIONAL_5 : Key
  KC_INTERNATIONAL_6 : Key
  KC_INTERNATIONAL_7 : Key
  KC_INTERNATIONAL_8 : Key
  KC_INTERNATIONAL_9 : Key
  KC_INTERNATIONAL_0 : Key
  KC_LANGUAGE_1 : Key
  KC_LANGUAGE_2 : Key
  KC_LANGUAGE_3 : Key
  KC_LANGUAGE_4 : Key
  KC_LANGUAGE_5 : Key
  KC_LANGUAGE_6 : Key
  KC_LANGUAGE_7 : Key
  KC_LANGUAGE_8 : Key
  KC_LANGUAGE_9 : Key
  KC_LANGUAGE_0 : Key
  KC_ALTERNATE_ERASE : Key
  KC_SYSTEM_REQUEST : Key
  KC_CANCEL : Key
  KC_CLEAR : Key
  KC_PRIOR : Key
  KC_RETURN : Key
  KC_SEPARATOR : Key
  KC_OUT : Key
  KC_OPER : Key
  KC_CLEAR_AGAIN : Key
  KC_CRSEL : Key
  KC_EXSEL : Key
  KC_LEFT_CTRL : Key
  KC_LEFT_SHIFT : Key
  KC_LEFT_ALT : Key
  KC_LEFT_GUI : Key
  KC_RIGHT_CTRL : Key
  KC_RIGHT_SHIFT : Key
  KC_RIGHT_ALT : Key
  KC_RIGHT_GUI : Key
  KC_SYSTEM_POWER : Key
  KC_SYSTEM_SLEEP : Key
  KC_SYSTEM_WAKE : Key
  KC_AUDIO_MUTE : Key
  KC_AUDIO_VOL_UP : Key
  KC_AUDIO_VOL_DOWN : Key
  KC_MEDIA_NEXT_TRACK : Key
  KC_MEDIA_PREV_TRACK : Key
  KC_MEDIA_STOP : Key
  KC_MEDIA_PLAY_PAUSE : Key
  KC_MEDIA_SELECT : Key
  KC_MEDIA_EJECT : Key
  KC_MEDIA_MAIL : Key
  KC_MAIL : Key
  KC_CALCULATOR : Key
  KC_MY_COMPUTER : Key
  KC_WWW_SEARCH : Key
  KC_WWW_HOME : Key
  KC_WWW_BACK : Key
  KC_WWW_FORWARD : Key
  KC_WWW_STOP : Key
  KC_WWW_REFRESH : Key
  KC_WWW_FAVORITES : Key
  KC_MEDIA_FAST_FORWARD : Key
  KC_MEDIA_REWIND : Key
  KC_BRIGHTNESS_UP : Key
  KC_BRIGHTNESS_DOWN : Key

%runElab derive "Key" [Generic, Meta, Show, Eq]

This basically doesn't terminate. I can't say how long this takes.

[stefan-hoeck]

Yes, the representation we use for sum types leads to a quadratic number of nested data constructors:

Z v
S(Z v)
S(S(Z v))
....

Type-checking these will therefore run in O(n^2) with relation to the number of data constructors of the sum type. If you know about a way to avoid this, that would be great as it would speed up things drastically, both a runtime and at compile-time.