T7453.hs:9:15: error:
    • Couldn't match type ‘r’ with ‘t’
        because type variable ‘t’ would escape its scope
      This (rigid, skolem) type variable is bound by
        the type signature for:
          z :: Id t
        at T7453.hs:8:11-19
      Expected type: Id t
        Actual type: Id r
    • In the expression: aux
      In an equation for ‘z’:
          z = aux
            where
                aux = Id v
      In an equation for ‘cast1’:
          cast1 v
            = runId z
            where
                z :: Id t
                z = aux
                  where
                      aux = Id v
    • Relevant bindings include
        aux :: Id r (bound at T7453.hs:10:21)
        z :: Id t (bound at T7453.hs:9:11)
        v :: r (bound at T7453.hs:7:7)
        cast1 :: r -> a (bound at T7453.hs:7:1)

T7453.hs:15:15: error:
    • Couldn't match type ‘r’ with ‘t1’
        because type variable ‘t1’ would escape its scope
      This (rigid, skolem) type variable is bound by
        the type signature for:
          z :: () -> t1
        at T7453.hs:14:11-22
      Expected type: () -> t1
        Actual type: () -> r
    • In the expression: aux
      In an equation for ‘z’:
          z = aux
            where
                aux = const v
      In an equation for ‘cast2’:
          cast2 v
            = z ()
            where
                z :: () -> t
                z = aux
                  where
                      aux = const v
    • Relevant bindings include
        aux :: forall b. b -> r (bound at T7453.hs:16:21)
        z :: () -> t1 (bound at T7453.hs:15:11)
        v :: r (bound at T7453.hs:13:7)
        cast2 :: r -> t (bound at T7453.hs:13:1)

T7453.hs:21:15: error:
    • Couldn't match expected type ‘t1’ with actual type ‘r’
        because type variable ‘t1’ would escape its scope
      This (rigid, skolem) type variable is bound by
        the type signature for:
          z :: t1
        at T7453.hs:20:11-16
    • In the expression: v
      In an equation for ‘z’:
          z = v
            where
                aux = const v
      In an equation for ‘cast3’:
          cast3 v
            = z
            where
                z :: t
                z = v
                  where
                      aux = const v
    • Relevant bindings include
        aux :: forall b. b -> r (bound at T7453.hs:22:21)
        z :: t1 (bound at T7453.hs:21:11)
        v :: r (bound at T7453.hs:19:7)
        cast3 :: r -> forall t. t (bound at T7453.hs:19:1)