Skip to content

Hole fits don't work for linear constructors

Consider:

data T = MkT Int Bool

nonlinT :: Int -> Bool -> T
nonlinT = _
linT :: Int %1 -> Bool %1 -> T
linT = _
mixT1 :: Int -> Bool %1 -> T
mixT1 = _
mixT2 :: Int %1 -> Bool -> T
mixT2 = _

We should suggest MkT as a valid hole fit for all 4 examples, but currently we only suggest it for nonlinT. This is because the hole fit machinery is given the dataConNonlinearType for the data constructor, so it can't be suggested in any cases where we want the linearity.

I am fixing this in !14357 (closed) by instead passing the original linear data con type to the hole fits computation; the subtype check (as extended to deal with multiplicities in that MR) then does the right thing.

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