type-tests.dx

'TODO: improve these "ambiguous type" error messages. The problem is that they
expose the core IR to show where the ambiguous types appear. We might be able to
improve things by recording source information when we create fresh inference
variables. Solving fully (insisting on no ambiguity) at each decl might also
help make the errors more local.

-- :t \x. x
-- > Type error:Ambiguous type variables: [?]
-- >
-- > ((_ans_ @> _ans_), [_ans_:(?->?) = \x:?. x])

-- :t \x. sum for i. x.i
-- > Type error:Ambiguous type variables: [?3]
-- >
-- > ( (_ans_ @> _ans_)
-- > , [ _ans_:((?3=>Float)->Float) = \x:(?3=>Float).
-- >   tmp:((?3=>Float)->Float) = (sum) (?3)
-- >   tmp1:(?3=>Float) = for \i:?3. (x) (i)
-- >   (tmp) (tmp1) ] )

-- :t \f x y. f y x
-- > Type error:Ambiguous type variables: [?3, ?6, ?7]
-- >
-- > ( (_ans_ @> _ans_)
-- > , [ _ans_:((?3->(?6->?7))->(?6->(?3->?7))) = \f:(?3->(?6->?7)). \x:?6. \y:?3.
-- >   tmp:(?6->?7) = (f) (y)
-- >   (tmp) (x) ] )

-- :t \x. for i j. x.j.i
-- > Type error:Ambiguous type variables: [?3, ?6, ?7]
-- >
-- > ( (_ans_ @> _ans_)
-- > , [ _ans_:((?3=>(?6=>?7))->(?6=>(?3=>?7))) = \x:(?3=>(?6=>?7)). for \i:?6. for \j:?3.
-- >   tmp1:(?6=>?7) = (x) (j)
-- >   (tmp1) (i) ] )

-- :t \f x. f x
-- > Type error:Ambiguous type variables: [?2, ?3]
-- >
-- > ((_ans_ @> _ans_), [_ans_:((?2->?3)->(?2->?3)) = \f:(?2->?3). \x:?2. (f) (x)])

-- :t \x. for (i,j). x.i.j
-- > Type error:Ambiguous type variables: [?4, ?7, ?8]
-- >
-- > ( (_ans_ @> _ans_)
-- > , [ _ans_:((?4=>(?7=>?8))->((?4 & ?7)=>?8)) = \x:(?4=>(?7=>?8)). for \pat:(?4 & ?7).
-- >   tmp1:?4 = %fst pat
-- >   tmp2:?7 = %snd pat
-- >   tmp3:(?7=>?8) = (x) (tmp1)
-- >   (tmp3) (tmp2) ] )

:t
   myid : a:Type ?-> a -> a = \x. x
   myid (myid) (myid 1)
> Int32

:t
   x = iota (Fin 10)
   sum x
> Int32

:t
   x = iota (Fin 10)
   y = iota (Fin 3)
   IToF (sum for i. x.i) + IToF (sum for j. y.j)
> Float32

:t
   x = iota (Fin 10)
   y = iota (Fin 3)
   sum for i. x.i + y.i
> Type error:
> Expected: (Fin 3)
>   Actual: (Fin 10)
>
>    sum for i. x.i + y.i
>                       ^

Narr = Fin 10

arr  = iota Narr

xr = map IToF arr

:t arr
> ((Fin 10) => Int32)

:t (\(x, y). x + y) (1.0, 2.0)
> Float32

:t
   f = \(x, y). x + 2.0 * y
   z = for i. (xr.i, xr.i * xr.i)
   sum (for i. f z.i)
> Float32

:t [1, 2, 3]
> ((Fin 3) => Int32)

:t [1, [2]]
> Type error:
> Expected: Int32
>   Actual: ((Fin 1) => Int32)
> If attempting to construct a fixed-size table not indexed by 'Fin n' for some n, this error may indicate there was not enough information to infer a concrete index set; try adding an explicit annotation.
>
> :t [1, [2]]
>        ^^^

:t [[1, 2], [3, 4]]
> ((Fin 2) => (Fin 2) => Int32)

:t [[1, 2], [3]]
> Type error:
> Expected: ((Fin 2) => Int32)
>   Actual: ((Fin 1) => Int32)
> If attempting to construct a fixed-size table not indexed by 'Fin n' for some n, this error may indicate there was not enough information to infer a concrete index set; try adding an explicit annotation.
>
> :t [[1, 2], [3]]
>             ^^^

f : Int -> Float =
 \x.
   z = x + 1.0
   x
> Type error:
> Expected: Int32
>   Actual: Float32
>
>    z = x + 1.0
>            ^^^

:t
   x = 3
   for i:Foo. 0
> Error: variable not in scope: Foo
>
>    for i:Foo. 0
>          ^^^


MyInt = Int
MyInt2 = MyInt

x : MyInt2 = 1

MyPair : Type -> Type =
  \a. (a & a)

:p
  pairs : (MyPair Int & MyPair Float) =
    ((1, 2), (1.0, 2.0))

  pairs
> ((1, 2), (1., 2.))


-- TODO: put source annotation on effect for a better message here
fEff : Unit -> {| a} a = todo
> Type error:
> Expected: Type
>   Actual: EffKind
>
> fEff : Unit -> {| a} a = todo
>                      ^^

:p
    for i:(Fin 7). sum for j:(Fin unboundName). 1.0
> Error: variable not in scope: unboundName
>
>     for i:(Fin 7). sum for j:(Fin unboundName). 1.0
>                                   ^^^^^^^^^^^

-- differentCaseResultTypes : Either Int Float -> Float
-- differentCaseResultTypes x = case x
--   Left f -> f
--   Right i -> i
-- > Type error:
-- > Expected: Int
-- >   Actual: Float
-- > In: i
-- >
-- >   Right i -> i
-- >              ^

-- inferEither x = case x
--     Left i -> i + 1
--     Right f -> floor f

-- caseEffects : wRef:(Ref Float) -> (Either Int Float) -> {Writer wRef} ()
-- caseEffects ref x = case x
--     Left  i -> ()
--     Right r -> ref := r
-- > Type error:
-- > Expected: { }
-- >   Actual: {State ref | ?_28}
-- > In: (ref := r)
-- >
-- >     Right r -> ref := r
-- >                    ^^^

-- :p (\(u,v). for i:0...u. 1.0) (2, 3)
-- > Type error:Function's result type cannot depend on a variable bound in an argument pattern
-- >
-- > :p (\(u,v). for i:0...u. 1.0) (2, 3)
-- >     ^^^^^^^^^^^^^^^^^^^^^^^^

g : a -> a = \x. x

:t g
> ((a:Type) ?-> a -> a)

:t
  f = \x:Int. x
  f 1
> Int32

:t
   f = \x:Float. x
   f 1
> Type error:
> Expected: Float32
>   Actual: Int32
>
>    f 1
>      ^

g1 : (a -> Int) -> (a -> Int) = \x. x

:t g1
> ((a:Type) ?-> (a -> Int32) -> a -> Int32)

g2 : a -> a = \x. idiv x x
> Type error:Couldn't synthesize a class dictionary for: (Integral a)
>
> g2 : a -> a = \x. idiv x x
>                   ^^^^^

h : (a -> b) -> (a -> b) = \x. x

:t h
> ((a:Type) ?-> (b:Type) ?-> (a -> b) -> a -> b)

fun : a -> a = \x. sin x
> Type error:Couldn't synthesize a class dictionary for: (Floating a)
>
> fun : a -> a = \x. sin x
>                    ^^^^

data NewPair a:Type b:Type = MkNewPair a b

fromNewPair : NewPair a b -> (a & b) = \(MkNewPair x y). (x, y)

newPair : NewPair Int Float = MkNewPair 1 2.0

:p fst newPair
> Type error:
> Expected: (a & b)
>   Actual: (NewPair Int32 Float32)
> (Solving for: [a:Type, b:Type])
>
> :p fst newPair
>        ^^^^^^^

:p fst $ fromNewPair newPair
> 1

:p NewPair
> NewPair

-- TODO: these are broken since switching from newtype mechanism to ADTs

-- :p NewPair Int
-- > NewPair Int

-- :p NewPair Int Float
-- > NewPair Int Float

-- NewPairIntFloat = NewPair Int Float

-- :p NewPairIntFloat
-- > NewPair Int Float

-- newPair2 : NewPairIntFloat = MkNewPair 1 2.0

-- :p fst $ fromNewPair newPair
-- > 1

good_range : Type = (1@Fin 3)..(2@_)

bad_range : Int = (1@Fin 3)..(2@_)
> Type error:
> Expected: Int32
>   Actual: Type
>
> bad_range : Int = (1@Fin 3)..(2@_)
>                            ^^


-- Tests for the Unit index set

() == ()
> True

() < ()
> False

() > ()
> False

() + ()
> ()

() - ()
> ()

() * ()
> ()

5.0 .* ()
> ()

-- Tests for Bool
:p True == True
> True
:p False == True
> False

:p (\x:Int. x) == (\x:Int. x)
> Type error:Couldn't synthesize a class dictionary for: (Eq (Int32 -> Int32))
>
> :p (\x:Int. x) == (\x:Int. x)
>                ^^^

def getFst1 (n:Type) ?-> (xs:n=>b) : b =
  xs.(fromOrdinal n 0)

:p getFst1 [1,2,3]
> 1

def getFst2 (xs:n=>b) : b =
  xs.(fromOrdinal n 0)

:p getFst2 [1,2,3]
> 1

def getFst3 (b:Type) ?-> (n:Type) ?-> (xs:n=>b) : b =
  xs.(fromOrdinal n 0)

:p getFst3 [1,2,3]
> 1

def triRefIndex (ref:Ref h (i':n=>(..i')=>Float)) (i:n) : Ref h ((..i)=>Float) =
  %indexRef ref i

(for i:(Fin 5). for j:(i..). 0.0).(0@_)
> Type error:Dependent functions can only be applied to fully evaluated expressions. Bind the argument to a name before you apply the function.
>
> (for i:(Fin 5). for j:(i..). 0.0).(0@_)
>                                    ^^^

-- Type inference of arguments always happens in checking mode, but the checking
-- doesn't provide any insight into what the argument is in this case. This checks
-- that type inference is able to realize that and switch to inference mode, so that
-- it can correctly infer the full dependent type.
--
-- There was a time when this wasn't possible, because checking mode would unify the
-- input type with a non-dependent function type, leading to a later unification errors.
id (for i:(Fin 2). for j:(..i). 1.0)
> [[1.]@(..(0@Fin 2)), [1., 1.]@(..(1@Fin 2))]

def weakerInferenceReduction (l : i:n=>(..i)=>Float) (j:n): Unit =
  for i:(..j).
    i' = %inject i
    for k:(..i').
      l.i'.k
    ()
  ()

-- Tests for table

a = [0, 1]
b = [0, 1]

:p a == b
> True

c = [1, 2]

:p a < c
> True