{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE TypeFamilies          #-}

module T4903a where

import Data.Kind

class El phi ix where
  proof :: phi ix

class Fam phi where
  from :: phi ix -> ix -> PF phi I0 ix

type family PF (phi :: Type -> Type) :: (Type -> Type) -> Type -> Type

data I0 a = I0 a

data I xi      (r :: Type -> Type) ix = I (r xi)
data (f :*: g) (r :: Type -> Type) ix = f r ix :*: g r ix

class HEq phi f where
  heq :: (forall ix. phi ix -> r ix -> Bool)
      -> phi ix -> f r ix -> Bool

instance El phi xi => HEq phi (I xi) where
  -- Replacing proof by undefined solves the problem
  heq eq _ (I x)     = eq proof x

instance (HEq phi f, HEq phi g) => HEq phi (f :*: g) where
  -- The problem only arises when there are two calls to heq here
  heq eq p (x :*: y) = heq eq p x && heq eq p y


{-# INLINABLE eq #-}
eq :: (Fam phi, HEq phi (PF phi)) => phi ix -> ix -> Bool  
eq p x = heq (\p (I0 x) -> eq p x) p (from p x)


data Tree = Bin Tree Tree

tree :: Tree
-- The problem only occurs on an inifite (or very large) structure  
tree = Bin tree tree

data TreeF :: Type -> Type where Tree :: TreeF Tree

type instance PF TreeF = I Tree :*: I Tree
-- If the representation is only |I Tree| then there is no problem

instance Fam TreeF where
  from Tree (Bin l r) = I (I0 l) :*: I (I0 r)

instance El TreeF Tree where proof = Tree