module MinimalExample where

open import Data.Vec
open import Data.String
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)

good : "x" ≢ "y"
good ()

bad : "x" ≢ Data.Vec.head ("y" ∷ "y" ∷ []) 
bad ()

{-
Failed to solve the following constraints:
  Is empty: "x" ≡ head ("y" ∷ "y" ∷ [])
      [ at <...snip...>/MinimalExample.agda:11,5-7 ]
-}