failure to normalize type, but REPL knows better

[dspivak]

Hi, I'm new to Idris. I've really enjoyed it so far, thanks!

I've encountered a strange bug, where the compiler complains that type T is different from Double, but when I ask the repl what T is, it responds that T is indeed Double.

Here is a quote from the repl, substituting T = state (Diffeq n f):

Type checking ./delme.idr
delme.idr:382:18-42:
    |
382 | DiffStream n f = run (Diffeq n f) refl 1.0
    |                  ~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of DiffStream with expected type
        Stream (pos (body (Diffeq n f)))

When checking an application of function Main.run:
        Type mismatch between
                Double (Type of 1.0)
        and
                state (Diffeq n f) (Expected type)

Holes: Main.DiffStream
*delme> :let f : Double -> Double
Holes: Main.DiffStream
*delme> :let n : Nat
Holes: Main.DiffStream
*delme> state (Diffeq n f)
Double : Type
Holes: Main.DiffStream
*delme>

As you can see, it complains that 1.0 is of type Double, whereas we need something of type "state (Diffeq n f)". However, the REPL shows that "state (Diffeq n f)" indeed normalizes to Double.

The code is below; I'm sorry that it's pretty far from minimal.

CODE:

module Main

import Data.Vect
%access public export

--- Objects ---
record Arena where
       constructor MkArena
       pos : Type
       dis : pos -> Type

--- Morphisms---

record Lens (dom : Arena) (cod : Arena) where
       constructor MkLens
       observe   : pos dom -> pos cod
       interpret : (p : pos dom) -> dis cod (observe p) -> dis dom p

--- Identity ---

idLens : (a : Arena) -> Lens a a
idLens a = MkLens id (\_ => id)


--- Composition ---

infixr 4 <.>
(<.>) : Lens a2 a3 -> Lens a1 a2 -> Lens a1 a3
(<.>) work23 work12 = MkLens obs int
      where
        obs : pos a1 -> pos a3
        obs = (observe work23) . (observe work12)

        int : (p : pos a1) -> (dis a3 (obs p)) -> dis a1 p
        int p = (interpret work12 p) . (interpret work23 (observe work12 p))

--- Special Arenas ---

IOArena : (i : Type) -> (o : Type) -> Arena --positions as output and
IOArena i o = MkArena o (\_ => i)           --distinctions as input

Self : Type -> Arena
Self s = IOArena s s

Closed : Arena
Closed = IOArena () ()

--- Reflections to Type ---

motor : Type -> Arena
motor t = IOArena () t

sensor : Type -> Arena
sensor t = IOArena t ()

motorFunction : {t, u : Type} -> (t -> u) -> Lens (motor t) (motor u)
motorFunction {t} {u} f = MkLens f (\_ => id) 

reflect : Arena -> Type
reflect a = Lens a Closed


--- Circle product ---

infixr 4 @@
(@@) : Arena -> Arena -> Arena
(@@) a b = MkArena posab disab
          where
            posab : Type
            posab = (p : pos a ** dis a p -> pos b)
            disab : posab -> Type
            disab (p ** f) = (d : dis a p ** dis b (f d))



circLens : {a1 : Arena} -> {b1 : Arena} -> {a2 : Arena} -> {b2 : Arena} -> 
           Lens a1 b1 -> Lens a2 b2 -> Lens (a1 @@ a2) (b1 @@ b2)
circLens {a1} {b1} {a2} {b2} l1 l2 = MkLens o i
          where
            o : pos (a1 @@ a2) -> pos (b1 @@ b2)
            o (p ** f) = (observe l1 p ** (observe l2) . f . (interpret l1 p))
            i : (p : pos (a1 @@ a2)) -> dis (b1 @@ b2) (o p) -> dis (a1 @@ a2) p
            i (p ** f) (d1 ** d2) = (e1 ** interpret l2 (f e1) d2)
            where
              e1 : dis a1 p 
              e1 = interpret l1 p d1

CircPow : Arena -> Nat -> Arena
CircPow _  Z     = Closed
CircPow a (S n) = a @@ CircPow a n 

CircPowLens : {a : Arena} -> {b : Arena} -> 
              Lens a b -> (n : Nat) -> Lens (CircPow a n) (CircPow b n)
CircPowLens {a} {b} _     Z    = idLens Closed 
CircPowLens {a} {b} lens (S n) = circLens lens (CircPowLens lens n)

motorPow : (t : Type) -> (n : Nat) -> Lens (CircPow (motor t) n) (motor (Vect n t))
motorPow t Z = MkLens (\_ => Nil) (\_, _ => ())


record Dynam where
       constructor MkDynam
       state : Type
       body   : Arena
       work   : Lens (Self state) body

run : (d : Dynam) -> reflect (body d) -> (state d) -> Stream (pos $ body d)
run d e s = outp :: (run d e next)
        where
          outp : pos $ body d
          next : state d
          outp = observe (work d) s
          next = interpret (work d) s $ interpret e outp ()

counit : (s : Type) -> Lens (Self s) Closed
counit s = MkLens o i
          where
            o : s -> ()
            o _ = ()
            i : s -> () -> s
            i s _ = s

comult : (s : Type) -> Lens (Self s) ((Self s) @@ (Self s))
comult s = MkLens o i
          where
            o : s -> pos ((Self s) @@ (Self s))
            o x = (x ** id)
            i : (x : s) -> (dis ((Self s) @@ (Self s)) (o x)) -> s
            i x (d1 ** d2) = d2

comultPow : (s : Type) -> (n : Nat) -> Lens (Self s) (CircPow (Self s) n)
comultPow s  Z    = counit s
comultPow s (S n) = (circLens (idLens (Self s)) (comultPow s n)) <.> (comult s)


install : (d : Dynam) -> (a : Arena) -> Lens (body d) a -> Dynam
install d a l = MkDynam (state d) a (l <.> (work d))

speedUp : Dynam -> Nat -> Dynam
speedUp dyn n = MkDynam (state dyn) fastBody fastWork
            where
              fastBody   : Arena
              fastWork   : Lens (Self $ state dyn) fastBody
              fastBody   = CircPow (body dyn) n
              fastWork   = CircPowLens (work dyn) n <.> comultPow (state dyn) n
 

PreDiffeq : Nat -> (Double -> Double)-> Dynam
PreDiffeq ll f = MkDynam Double (motor Double) lens 
            where 
              lens : Lens (Self Double) (motor Double)
              lens = MkLens id interp
              where
                l : Double
                l = cast $ toIntNat ll
                interp : Double -> () -> Double
                interp x _ = x + (f x)/l

Diffeq : Nat -> (Double -> Double) -> Dynam
Diffeq n f = install fastdyn fastbody lens 
        where
          fastdyn : Dynam
          fastdyn = speedUp (PreDiffeq n f) n
          fastbody : Arena
          fastbody = motor (Vect n Double)
          lens : Lens (CircPow (motor Double) n) fastbody
          lens = motorPow Double n

DiffStream : (n : Nat) -> (f : Double -> Double) -> Stream (pos (body (Diffeq n f)))
DiffStream n f = run (Diffeq n f) refl start
        where
          start : state (Diffeq n f)
          start = 1.0                        --argh, should work
          refl  : reflect (body (Diffeq n f))