Strange Typeable error message involving TypeInType (#13872) · Issues · Glasgow Haskell Compiler / GHC

Strange Typeable error message involving TypeInType

I originally discovered this when tinkering with #13871 (closed). This program:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where

import Data.Kind
import Data.Typeable

data Foo (a :: Type) (b :: Type) where
  MkFoo :: (a ~ Int, b ~ Char) => Foo a b

data family Sing (a :: k)
data SFoo (z :: Foo a b) where
  SMkFoo :: SFoo MkFoo

f :: String
f = show $ typeOf SMkFoo

Fails in GHC 8.0.1, 8.0.2, and 8.2 (after applying D3671) with a rather unsightly error message:

GHCi, version 8.3.20170624: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo              ( Foo.hs, interpreted )

Foo.hs:19:12: error:
    • No instance for (Typeable <>) arising from a use of ‘typeOf’
    • In the second argument of ‘($)’, namely ‘typeOf SMkFoo’
      In the expression: show $ typeOf SMkFoo
      In an equation for ‘f’: f = show $ typeOf SMkFoo
   |
19 | f = show $ typeOf SMkFoo
   |            ^^^^^^^^^^^^^

I'm not sure what this mysterious <> is, but I'm pretty sure it shouldn't be making an appearance here. (See also #13780 (closed), where <> also makes a surprise guest appearance.)

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

I originally discovered this when tinkering with #13871. This program:

```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where

import Data.Kind
import Data.Typeable

data Foo (a :: Type) (b :: Type) where
  MkFoo :: (a ~ Int, b ~ Char) => Foo a b

data family Sing (a :: k)
data SFoo (z :: Foo a b) where
  SMkFoo :: SFoo MkFoo

f :: String
f = show $ typeOf SMkFoo
```

Fails in GHC 8.0.1, 8.0.2, and 8.2 (after applying [D3671](https://phabricator.haskell.org/D3671)) with a rather unsightly error message:

```
GHCi, version 8.3.20170624: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo              ( Foo.hs, interpreted )

Foo.hs:19:12: error:
    • No instance for (Typeable <>) arising from a use of ‘typeOf’
    • In the second argument of ‘($)’, namely ‘typeOf SMkFoo’
      In the expression: show $ typeOf SMkFoo
      In an equation for ‘f’: f = show $ typeOf SMkFoo
   |
19 | f = show $ typeOf SMkFoo
   |            ^^^^^^^^^^^^^
```

I'm not sure what this mysterious `<>` is, but I'm pretty sure it shouldn't be making an appearance here. (See also #13780, where `<>` also makes a surprise guest appearance.)

<details><summary>Trac metadata</summary>

| Trac field             | Value                   |
| ---------------------- | ----------------------- |
| Version                | 8.0.1                   |
| Type                   | Bug                     |
| TypeOfFailure          | OtherFailure            |
| Priority               | normal                  |
| Resolution             | Unresolved              |
| Component              | Compiler (Type checker) |
| Test case              |                         |
| Differential revisions |                         |
| BlockedBy              |                         |
| Related                |                         |
| Blocking               |                         |
| CC                     |                         |
| Operating system       |                         |
| Architecture           |                         |

</details>