Test.idr

module Test

import Data.Fin

record AttemptA where
  constructor ConstructA
  goA : (n : Nat) -> Fin n -> Fin n

record AttemptB where
  constructor ConstructB
  goB : Fin n -> Fin n

record AttemptC where
  constructor ConstructC
  goC : {n : Nat} -> Fin n -> Fin n

  -- Test.idr line 13 col 7:
  -- When checking right hand side of Test.AttemptC.goC with expected type
  -- Fin n -> Fin n

  -- Type mismatch between
  --   Fin n1 -> Fin n1 (Type of goC)
  -- and
  --   Fin n -> Fin n (Expected type)

  -- Specifically:
  -- Type mismatch between
  --   Nat
  -- and
  --   Fin n