Skip to content

Another loop with injective type families

Broken out from #16512 (closed), the following program causes GHC to loop:

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators, AllowAmbiguousTypes          #-}

module T16512 where

-- This test is significantly abbreviated from what was posted; see
-- #16512 for more context.

type family Dim v

type family v `OfDim` (n :: Dim v) = r | r -> n

(!*^) :: Dim m `OfDim` j -> Dim m `OfDim` i
(!*^) = undefined

The fix for #16512 (closed) does not fix this.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information