idrisfailure.idr

namespace thisWorks
  testMyErased : Exists {type = (Nat, String)} (\y => (String, (Nat, Nat)))

  0 testMyUse : String
  testMyUse = Builtin.fst $ snd $ testMyErased

  0 testMyUse2 : (Nat, Nat)
  testMyUse2 = Builtin.snd $ snd testMyErased
  
  
namespace thisFails
  testMyErased : Exists {type = (Nat, String)} (\(y, z) => (String, (Nat, Nat)))

  0 testMyUse : String
  testMyUse = Builtin.fst $ snd $ testMyErased
  {-
  While processing right hand side of testMyUse.
  Can't solve constraint between:
  let (y, z) = fst testMyErased in (String, (Nat, Nat)) and (String, ?b)
  -}

  0 testMyUse2 : (Nat, Nat)
  testMyUse2 = Builtin.snd $ snd testMyErased