Merge pull request #1092 from agda/jesper-eta

Eta-expand definition of `pure` in Data.Erased in response to agda/agda#4432

Author: jespercockx

src/Data/Erased.agda

@@ -36,7 +36,7 @@ map : (A → B) → Erased A → Erased B
 map f [ a ] = [ f a ]
 
 pure : A → Erased A
-pure = [_]
+pure x = [ x ]
 
 infixl 4 _<*>_
 _<*>_ : Erased (A → B) → Erased A → Erased B