Clash error call: `zipEqual: left list is longer` when using custom type proof

[martijnbastiaan]

The following:

module Test where

import Clash.Prelude
import Data.Constraint
import Data.Proxy
import Unsafe.Coerce

data T depth = T (BitVector depth) deriving (Generic)

instance (1 <= CLog 2 depth, KnownNat depth) => NFDataX (T depth)

-- | if (2 <= n) holds, then (1 <= CLog 2 n) also holds.
oneLeCLog2n :: forall n . (2 <= n) => Proxy n -> Dict (1 <= CLog 2 n)
oneLeCLog2n Proxy = unsafeCoerce (Dict :: Dict ())

f ::
  forall dom depth.
  ( HiddenClockResetEnable dom
  , KnownNat depth
  , 2 <= depth ) =>
  Proxy depth ->
  Signal dom Bool ->
  Signal dom Bool
f Proxy =
  case oneLeCLog2n (Proxy @depth) of
    Dict -> mealy go (T 0)

 where
  go :: T depth -> Bool -> (T depth, Bool)
  go (T n) True = (T (n + 1), False)
  go (T n) False = (T (n - 1), True)
{-# NOINLINE f #-}

topEntity clk rst ena =
  withClockResetEnable clk rst ena $
    f @System @2 Proxy
{-# NOINLINE topEntity #-}

causes:

<no location info>: error:
    Clash error call:
    zipEqual: left list is longer
    CallStack (from HasCallStack):
      error, called at src/Data/List/Extra.hs:124:19 in clash-lib-1.7.0-inplace:Data.List.Extra
      zipEqual, called at src/Clash/Normalize/Transformations/Case.hs:203:19 in clash-lib-1.7.0-inplace:Clash.Normalize.Transformations.Case
      caseCon', called at src/Clash/Normalize/Transformations/Case.hs:149:32 in clash-lib-1.7.0-inplace:Clash.Normalize.Transformations.Case
      caseCon, called at src/Clash/Normalize/Strategy.hs:91:36 in clash-lib-1.7.0-inplace:Clash.Normalize.Strategy

In other examples Clash introduces free variables in caseCon (but I've yet to make a small reproducer for that).

Printing the arguments given to zipEqual gives:

xs1: [ Id
    { varName =
        Name
          { nameSort = Internal
          , nameOcc = "c$sel"
          , nameUniq = 2
          , nameLoc = UnhelpfulSpan UnhelpfulNoLocationInfo
          }
    , varUniq = 2
    , varType =
        AppTy
          (AppTy
             (AppTy
                (AppTy
                   (ConstTy
                      (TyCon
                         Name
                           { nameSort = User
                           , nameOcc = "GHC.Prim.~#"
                           , nameUniq = 3674937295934324842
                           , nameLoc = UnhelpfulSpan UnhelpfulNoLocationInfo
                           }))
                   (ConstTy
                      (TyCon
                         Name
                           { nameSort = User
                           , nameOcc = "GHC.Types.Bool"
                           , nameUniq = 3674937295934324744
                           , nameLoc =
                               RealSrcSpan SrcSpanMultiLine "Test.hs" 16 1 23 18 Nothing
                           })))
                (ConstTy
                   (TyCon
                      Name
                        { nameSort = User
                        , nameOcc = "GHC.Types.Bool"
                        , nameUniq = 3674937295934324744
                        , nameLoc =
                            RealSrcSpan SrcSpanMultiLine "Test.hs" 16 1 23 18 Nothing
                        })))
             (AppTy
                (AppTy
                   (ConstTy
                      (TyCon
                         Name
                           { nameSort = User
                           , nameOcc = "GHC.TypeNats.<=?"
                           , nameUniq = 3674937295934325074
                           , nameLoc =
                               RealSrcSpan SrcSpanMultiLine "Test.hs" 16 1 23 18 Nothing
                           }))
                   (LitTy (NumTy 1)))
                (AppTy
                   (AppTy
                      (ConstTy
                         (TyCon
                            Name
                              { nameSort = User
                              , nameOcc = "GHC.TypeLits.Extra.CLog"
                              , nameUniq = 8214565720323785211
                              , nameLoc =
                                  RealSrcSpan SrcSpanMultiLine "Test.hs" 16 1 23 18 Nothing
                              }))
                      (LitTy (NumTy 2)))
                   (LitTy (NumTy 2)))))
          (ConstTy
             (TyCon
                Name
                  { nameSort = User
                  , nameOcc = "GHC.Types.True"
                  , nameUniq = 3891110078048108586
                  , nameLoc =
                      RealSrcSpan SrcSpanMultiLine "Test.hs" 16 1 23 18 Nothing
                  }))
    , idScope = LocalId
    }
]
left args: []

Workaround: add NOINLINE to oneLeCLog2n

[christiaanb]

Looking at the log, the culprit is quite clearly the unsafeCoerce (Dict :: Dict ()):

case GHC.Classes.(%%)[7854277750134145024] of
  GHC.Types.Eq#[3891110078048108571]
    (c$sel[2] :: GHC.Prim.~#[3674937295934324842]
                   GHC.Types.Bool[3674937295934324744]
                   GHC.Types.Bool[3674937295934324744]
                   (Data.Type.Ord.OrdCond[8214565720323786066]
                      GHC.Types.Bool[3674937295934324744]
                      (Data.Type.Ord.Compare[8214565720323786076]
                         GHC.Num.Natural.Natural[3674937295934324786]
                         1
                         (GHC.TypeLits.Extra.CLog[8214565720323786119]
                            2
                            2))
                      GHC.Types.True[3891110078048108586]
                      GHC.Types.True[3891110078048108586]
                      GHC.Types.False[3891110078048108556])
                   GHC.Types.True[3891110078048108586]) ->
    c$sel[2][LocalId]

which comes from:

  case oneLeCLog2n (Proxy @depth) of
    Dict -> mealy go (T 0)

i.e. the type of the case subject should be something of an equality constraint, but the unsafeCoerce gave us a GHC.Classes.(%%).

[martijnbastiaan]

To conclude this issue: this is really a PBKAC. The first type argument of Dict is pretty important and needs to conform to your proof. E.g., the proof introduced in the first message should read:

oneLeCLog2n :: forall n . (2 <= n) => Proxy n -> Dict (1 <= CLog 2 n)
oneLeCLog2n Proxy = unsafeCoerce (Dict :: Dict (1 <= 1))

[leonschoorl]

Or we could make caseCon a little more careful

[leonschoorl]

It seemed easy it to look at dcUniqs instead of dcTags to fix #2376.

But on second thought this "fix" (silently) breaks other uses of unsafeCoerce, which used to work before.

data AB a b = A a    | B b
data CD     = C Bool | D Int

topEntity :: Int
topEntity = case unsafeCoerce ab of
  C _ -> 123
  D i -> i
 where
  ab :: AB Bool Int
  ab = B 4

caseCon now turns this into undefined because none of the alternatives match.

[martijnbastiaan]

We shouldn't try and detect this; unsafeCoerce is really when people want to do incredibly unsafe stuff. If they do it incorrectly (like showcased in this issue) they can expect anything from weird errors to segmentation faults. Based on that I think we should close this issue.

We should handle coercions between AB and CD gracefully though. But from the sounds of it we're already doing that. (?) If we're not that's probably grounds for opening an issue. (But TBF, I don't think it's particularly high priority. It's unsafe for a reason.)

[alex-mckenna]

Or we could make caseCon a little more careful

I don't think it makes sense to change how caseCon works, since the problem here is that the term level scrutinee did not line up with what the type said it should be. This only happens when

• using things which are unsafeCoerce and not being careful
• a transformation before caseCon is incorrect and has not preserved type-safety

I think a better idea would be to improve the error here, since the main problem other than programmer error was Clash not actually telling us what was wrong directly. We can inferCoreTypeOf the scrutinee of the expression, and get the types of patterns by examining

• the DataCon and [TyVar] for DataPat
• the Literal for LitPat

We can then say that

• all patterns should have the same codomain
• this type should be the same as the inferred type of the scrutinee

Note that this is equality is possibly up to normalizeType, i.e. type families may appear and ruin your day.