-- Copyright 2020-2021 Google LLC
--
-- Licensed under the Apache License, Version 2.0 (the "License");
-- you may not use this file except in compliance with the License.
-- You may obtain a copy of the License at
--
--      http://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-- See the License for the specific language governing permissions and
-- limitations under the License.

{-# OPTIONS -Wwarn=inaccessible-code #-}

module FinErrors where

import Data.Fin.Int (Fin)

x0 :: Fin 0
-- Want: out of range.
x0 = 0

x1, x2 :: Fin 2
-- Want: out of range.
x1 = 2
-- Want: out of range.
x2 = -2

x3 :: Fin 2 -> String
x3 x = case x of
  0 -> "hi"
  3 -> "want unreachable code" -- TODO these could have better error messages
  -1 -> "want unreachable code"
  _ -> "other"

-- Want: not sure it's in range
x4 :: Fin n
x4 = 42

-- Want: illegal -0
x5 :: Fin 1
x5 = -0

-- Since this literal overflows (LitRepr (Fin n) ~ Int), it's liable to
-- generate proof 18446744073709551618 < n when given any (2 :: Fin n), and
-- then make an ill-formed Fin of that value.  We have constraints on the
-- underlying LitRepr precisely to prevent this: because this literal cannot be
-- faithfully represented by LitRepr (Fin n), even if the instance for Fin n
-- thinks it can accept the literal, we must reject it.
x100 :: Fin n -> Fin n
x100 x = case x of
  18446744073709551618 -> 18446744073709551618
  _ -> x

-- This also needs to be a type error: if it matched (which it would for 2, if
-- we generated code for it), we would be able to create a proof that
-- 18446744073709551618 < n for any n > 2.
x101 :: Fin n -> Fin n
x101 x = case x of
  18446744073709551618 -> x
  _ -> x