[ #431 ] Eta-expand definition of rTail in EraseType.agda test case

Author: jespercockx

test/EraseType.agda

@@ -29,6 +29,6 @@ testCong = singCong (1 +_) testSingleton
 {-# COMPILE AGDA2HS testCong #-}
 
 rTail : ∀ {@0 x xs} → Singleton {a = List Int} (x ∷ xs) → Singleton xs
-rTail = singTail
+rTail ys = singTail ys
 
 {-# COMPILE AGDA2HS rTail #-}

test/golden/EraseType.hs

@@ -16,5 +16,5 @@ testCong :: Int
 testCong = 1 + testSingleton
 
 rTail :: [Int] -> [Int]
-rTail = \ ys -> tail ys
+rTail ys = tail ys