Skip to content

GHC doesn't terminate when solving a weird class instance

The following:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Test where

import GHC.TypeLits

data Pet (a :: k) = Pet
  { name :: String
  } deriving Show

class SetField (name :: Symbol) s t b | name t -> s b
                                      , name s -> t b where
  setField :: b -> s -> t

instance
  ( SetField "name" (Pet a) (Pet b) String
  ) => SetField "name" (Pet (a :: k)) (Pet (b :: k')) String where
  setField v d = d { name = v }

loop = setField @"name" 'c' (Pet "hi")

makes GHC 9.0.1 and HEAD loop. With 8.10.4 it properly terminates with an error:

TX.hs:27:8: error:
    • Couldn't match type ‘[Char]’ with ‘Char’
        arising from a functional dependency between:
          constraint ‘SetField "name" (Pet a) (Pet b) Char’
            arising from a use of ‘setField’
          instance ‘SetField "name" (Pet a1) (Pet b1) String’
            at TX.hs:(23,3)-(24,60)
    • In the expression: setField @"name" 'c' (Pet "hi")
      In an equation for ‘loop’: loop = setField @"name" 'c' (Pet "hi")
   |
27 | loop = setField @"name" 'c' (Pet "hi")
   |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Either changing the kind of b to k or the instance to

instance
  ( SetField "name" (Pet a) (Pet b) x
  , x ~ String
  ) => SetField "name" (Pet (a :: k)) (Pet (b :: k')) x where
  setField v d = d { name = v }

makes it terminate again.

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