Recursive use of type-in-type results in infinite loop

Typechecking this module results in an infinite loop:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeInType #-}
module X where

data V a
data T = forall (a :: S). MkT (V a)
data S = forall (a :: T). MkS (V a)

There's a mutually recursive reference so it should be rejected but maybe the check is not happening early enough (or the existing check is only for self-reference.)

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

changed weight to 5

added Tbug Trac import typechecker labels

added TypeInType label

Probably a similar issue:

{-# LANGUAGE TypeInType #-}

import Data.Proxy

data A a = A (Proxy (a :: A))

results in *** Exception: stack overflow

mentioned in issue #12386 (closed)

CCing goldfire who will hopefully have some ideas.

Trac metadata

Trac field	Value
CC	- → goldfire

Yes -- I expect to take a look at this in my bug sweep, which will hopefully start next week or so.

c.f #12386 (closed)

changed milestone to %8.2.1

changed weight to 10

Trac metadata

Trac field	Value
Priority	normal → highest

mentioned in commit 03b0b8e4

closed

Works in HEAD. I doubt it's worth trying to track the fix down for the 8.0 branch.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	- → dependent/should_fail/T12714

Trac metadata

Trac field	Value
Test case	dependent/should_fail/T12714 → dependent/should_fail/T12174

added Phighest label

mentioned in merge request !4076 (closed)

mentioned in commit 05a765b3

mentioned in commit 760307cf