Skip to content

Combining type families and strict fields creates casts that clash can't handle #2961

@hiddemoll

Description

@hiddemoll

@leonschoorl and I created this minimal reproducer based on how I got this error while using Clash Protocols.

    Clash.Netlist(833): Not in normal form: application of cast
    
    (<prefixName>"waTop3"Clash.Sized.Internal.Index.fromInteger# @256 256 1) ▷
      Clash.Sized.Internal.Index.Index[8214565720323787678] 256
      ~
      GHC.Num.Integer.Integer[3674937295934324784]
{-# LANGUAGE TypeFamilyDependencies #-}
module Minimal where

import Clash.Explicit.Prelude
import Data.Data (Proxy)
import Data.Functor.Identity (Identity)
import Data.Kind (Type)

{- | Allows for optional data.
Depending on the value of @keep@, the data can either be included or left out.
When left out, the data is represented instead as type @()@.
-}
type family KeepType (keep :: Bool) (optionalType :: Type) = t | t -> keep optionalType where
  KeepType 'True optionalType = Identity optionalType
  KeepType 'False optionalType = Proxy optionalType

type BurstLengthType (keep :: Bool) = KeepType keep (Index 256)

data M2S_WriteAddress = M2S_WriteAddress !(BurstLengthType 'True)

waTop :: M2S_WriteAddress
waTop = M2S_WriteAddress 1 -- Clash casts this (Index 256) to an Integer
{-# OPAQUE waTop #-}
{-# ANN
  waTop
  ( defSyn "wa" )
  #-}

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions