content: {-# LANGUAGE RankNTypes, GADTs, TypeFamilies #-}
  module Test where 
  
  
  data T a where 
    MkT :: a -> T a 
    MkT2 :: forall a b. (b ~ T b) => b -> T a
    MkT3 :: forall a. (a ~ Bool) => T a 
  -- Occurs checks in givens
  foo :: forall a. (a ~ T a) => a -> a 
  foo x = x 
  
  blah x = case x of 
             MkT2 y -> ()
  
  -- Mismatches in givens 
  bloh :: T Int -> () 
  bloh x = case x of 
             MkT3 -> () 
  
  type family F a b 
  type family G a b
  type instance F a Bool = a 
  type instance G a Char = a
  
  goo1 :: forall a b. (F a b ~ [a]) => b -> a  -> a
  goo1 = undefined 
  
  goo2 :: forall a. G a Char ~ [Int] => a -> a
  goo2 = undefined
  
  -- Just an occurs check
  test1 = goo1 False undefined
  
  -- A frozen occurs check, now transformed to decomposition error
  test2 = goo2 (goo1 False undefined)
  test3 = goo1 False (goo2 undefined)
  
  
  -- A frozen occurs check, now transformed to both a decomposition and occurs check
  data M a where 
    M :: M a 
  data T2 a b where
    T2 :: T2 a b 
  
  goo3 :: forall a b. F a b ~ T2 (M a) a => b -> a -> a 
  goo3 = undefined
  
  goo4 :: forall a c. G a Char ~ T2 (T2 c c) c => a -> a
  goo4 = undefined 
  
  test4 = goo4 (goo3 False undefined)
  test5 = goo3 False (goo4 undefined)
  
  
  
  