Type Error Revealed in Slow Motion: Identical Functions Treated Differently

[paddytheplaster]

Hello,

I'm using Clash, version 1.3.0 (using clash-lib, version: 1.3.0).

The following shows a case where two functions 'ok' and 'fail', where 'fail = ok'. However, 'ok' type checks but 'fail' doesn't type check. However, when you use 'ok' you get a run-time error. In fact, 'clashi' accepts the definition of 'ok' but when you ask, 'clashi' can't infer the type of 'ok'.

clashi> :t ok

<interactive>:1:1: error:
Couldn't match type 'False with 'True arising from a use of `ok'

clashi> ok

<interactive>:1:1: error:
Couldn't match type 'False with 'True arising from a use of `ok'

The following is the code.

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
{-# OPTIONS -fconstraint-solver-iterations=0 #-}

module Ex where

import Clash.Prelude

-- type checks but fails at run time
ok :: forall (d :: Nat) (d' :: Nat)
     . (KnownNat d, d ~ 2, KnownNat d', d' ~ (1 - d))
    => SNat d'
    -> SNat d
    -> IO ( )
ok _ _ = return ( )

-- uncomment next line and this doesn't type check
-- fail = ok

Regards,

Paddy

[christiaanb]

This is correct. You're basically saying:

ok :: "You can only call me in a context where the natural number d' is equal to '-1'" => IO ()

Then when you to :t ok, you're basically asking: what is the type of the expression ok? (Note that if you want to know the type of the function ok you should use :i ok). Then the constraint solvers get to work, trying to solve the set of equations d' ~ (1 - d); d ~ 2. They get as far as 2 <=? 1 ~ True, which reduces to False ~ True; which is then the error that you get.

If you give fail the same type signature as ok, you won't get a type error, since fail then explicitly has the same context as ok. Another thing that might work is adding the {-# LANGUAGE NoMonomorphismRestriction #-} language pragma at the top of the file.

[christiaanb]

So the only constraints that arise from the definition of ok are Monad IO, a ~ () because of return :: Monad m =>a -> m a; and both of those constraints hold. You are then free to add as many constraints on top of that in the type signature, even ones that can never be satisfied (in a type correct program): the definition of ok is still type-correct.

[paddytheplaster]

This is correct. You're basically saying:

ok :: "You can only call me in a context where the natural number d' is equal to '-1'" => IO ()

Then when you to :t ok, you're basically asking: what is the type of the expression ok? (Note that if you want to know the type of the function ok you should use :i ok). Then the constraint solvers get to work, trying to solve the set of equations d' ~ (1 - d); d ~ 2. They get as far as 2 <=? 1 ~ True, which reduces to False ~ True; which is then the error that you get.

If you give fail the same type signature as ok, you won't get a type error, since fail then explicitly has the same context as ok. Another thing that might work is adding the {-# LANGUAGE NoMonomorphismRestriction #-} language pragma at the top of the file.

So the only constraints that arise from the definition of ok are Monad IO, a ~ () because of return :: Monad m =>a -> m a; and both of those constraints hold. You are then free to add as many constraints on top of that in the type signature, even ones that can never be satisfied (in a type correct program): the definition of ok is still type-correct.

Thanks, and thanks for the previous explanation. This makes sense but it's a bit counter-intuitive that fail is not the same as ok. Shouldn't any LHS in a definition of the form a = b which comes without a signature for a be equal to the RHS (including the type)?

Regards,

Paddy

[christiaanb]

It would... in the absence of the monomorphism restriction... but we decided to enable the monomorphism restriction: https://github.com/clash-lang/clash-compiler/issues/1270

Waveform generation using http://hackage.haskell.org/package/clash-prelude-1.2.5/docs/Clash-Signal-Trace.html is basically broken when the monomorphism restriction is disabled, and leaving it disabled (probably) negatively impacts Haskell-land simulation performance of Clash circuits.

And you can still achieve the same types with the monomorphism restriction enabled, just that sometimes you'll have to add an explicit type signature.

[paddytheplaster]

It would... in the absence of the monomorphism restriction... but we decided to enable the monomorphism restriction: #1270

Waveform generation using http://hackage.haskell.org/package/clash-prelude-1.2.5/docs/Clash-Signal-Trace.html is basically broken when the monomorphism restriction is disabled, and leaving it disabled (probably) negatively impacts Haskell-land simulation performance of Clash circuits.

And you can still achieve the same types with the monomorphism restriction enabled, just that sometimes you'll have to add an explicit type signature.

OK. Great. I'll have a look at that (and hopefully will keep that in mind).

Regards,

Paddy